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;
nnlf : Nat → Nat → List;
end enrich