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