proposition: Lemma imp_def : imp = (fun p : Prop => fun q : Prop => (p /\ q) = p).
proof: Proof. apply fun_ext; intro p. apply fun_ext; intro q. apply prop_ext. intro pq. apply prop_ext. intros [hp _]. exact hp. intro hp. split. exact hp. apply pq. exact hp. intro e. rewrite <- e. intros [_ hq]. exact hq. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts