proposition: Fact Forall_impl X (P Q : X -> Prop) ll : (forall x, In x ll -> P x -> Q x) -> Forall P ll -> Forall Q ll.
proof: Proof. intros H; induction 1 as [ | x ll Hx Hll IH ]; constructor. + apply H; simpl; auto. + apply IH; intros ? ?; apply H; simpl; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)