data specification
using nat, list-del
data types
Stream = ⌜ . ⌝(. .l : List) with finp
| ⌜ . ⌝(. .f : Nat → Elem)
;
variables
σ : Stream;
nf : Nat → Elem;
x : List;
m : Nat;
l : List;
f : Nat → Elem;
end data specification