proposition: Lemma all_def : forall {A : Type'}, (@all A) = (fun P : A -> Prop => P = (fun x : A => True)).
proof: Proof. intro A. apply fun_ext; intro p. apply prop_ext. intro h. apply fun_ext; intro x. apply prop_ext. intros _. exact I. intros _. exact (h x). intros e x. rewrite e. exact I. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts