proposition: Lemma app_cons_l : forall x l1 l2, (x::l1) ++ l2 = x :: (l1++l2).
proof: Proof. Proof using. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)