proposition: Lemma last_eq_last_inv : forall x1 x2 l1 l2, l1 & x1 = l2 & x2 -> l1 = l2 /\ x1 = x2.
proof: Proof. Proof using. introv H. gen l2. induction l1; introv E; rew_list in E. { destruct l2; rew_list in E; inverts E as E. { auto. } { false nil_eq_last_inv E. } } { destruct l2; rew_list in E. { inverts E as E. false last_eq_nil_inv E. } { inverts E. forwards* [? ?]: IHl1. split; congruence. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)