proposition: Lemma list_neq_nil_inv_cons : forall l, l <> nil -> exists x q, l = x :: q.
proof: Proof. Proof using. introv N. destruct* l. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)