proposition: Lemma all_func (A : Type) (P Q : A -> Prop) : (forall x, P x -> Q x) -> (forall x, P x) -> (forall x, Q x).
proof: Proof. intros allx_Px_to_Qx allx_Px x. exact ((allx_Px_to_Qx x) (allx_Px x)). Qed.
imports: Classical_Prop Classical_Pred_Type