proposition: Lemma Forall_cons_iff@{u} : forall (T : Type@{u}) (P : T -> Prop) a b, Forall P (a :: b) <-> (P a /\ Forall P b).
proof: Proof. clear. split. inversion 1; auto. destruct 1; constructor; auto. Qed.
imports: Coq.Lists.List ExtLib.Core.RelDec ExtLib.Structures.Monoid ExtLib.Structures.Reducible ExtLib.Tactics.Consider ExtLib.Tactics.Injection