proposition: Lemma cons_eq_middle_inv : forall x y l1 l2 l, x :: l = l1 & y ++ l2 -> (l1 = nil /\ x = y /\ l = l2) \/ (exists l1', l1 = x::l1').
proof: Proof. Proof using. intros. destruct l1; rew_list in H; inverts H. { left~. } { right*. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)