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