proposition: Lemma iapp_eq {A : Set} (l1 l1' l2 l2' : Σ n, ilist A n) : l1 = l1' -> l2 = l2' -> (_, iapp l1.2 l2.2) = (_, iapp l1'.2 l2'.2).
proof: Proof. now simplify *. Defined.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations