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