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