proposition: Lemma nil_eq_middle_inv : forall x l1 l2, nil = l1 & x ++ l2 -> False.
proof: Proof. Proof using. intros. destruct l1; inverts H. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)