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