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