fact: Definition remove_forall_eql_and A x (P : _ -> Prop) (Q : A -> Prop) : flip impl (forall y : A, (y = x /\ Q y) -> P y) (Q x -> P x) := proj2 (@iff_remove_forall_eql_and A x P Q).
imports: Coq.Program.Program Fiat.Common