proposition: Lemma list2_ind : forall A B (P:list A->list B->Prop) l1 l2, length l1 = length l2 -> P nil nil -> (forall x1 xs1 x2 xs2, length xs1 = length xs2 -> P xs1 xs2 -> P (x1::xs1) (x2::xs2)) -> P l1 l2.
proof: Proof. Proof using. introv E M1 M2. gen l2. induction l1 as [|x1 l1']; intros; destruct l2 as [|x2 l2']; try solve [false; math]; auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)