proposition: Lemma iapp_cons : forall (A : Set) (i j : nat) (l1 : ilist A i) (l2 : ilist A j) (x : A), iapp (Cons x l1) l2 = Cons x (iapp l1 l2).
proof: Proof. now simp iapp. Qed.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations