enrich
infinite-append
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