enrich
infinite-append-old
with
variables
nextli : list('a) → list('a);
nextnli : list('a) × nat → list('a);
x : list('a);
y : list('a);
a : 'a;
b : 'a;
σ : stream('a);
ii : nat → nat;
m : nat;
n : nat;
lf : nat → list('a);
end enrich