proposition: Lemma list2_ind_last : 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 (xs1&x1) (xs2&x2)) -> P l1 l2.
proof: Proof. Proof using. introv E M1 M2. gen l2. induction l1 using list_ind_last; [| rename a into x1, l1 into l1']; intros; destruct (last_case l2) as [|(x2&l2'&E2)]; subst; rew_list in *; try solve [false; math]; auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)