proposition: Lemma Forall_last_eq : forall P l x, Forall P (l & x) = (Forall P l /\ P x).
proof: Proof. Proof using. intros. extens. induction l; rew_list. { iff M (M1&M2). { inverts* M. } { autos*. } } { iff M (M1&M2). { inverts* M. } { inverts* M1. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)