Check conj. Check or_introl. Goal False <-> forall Z: Prop, Z. Proof. split. - intros []. - intros f. exact (f False). Show Proof. Qed. Goal forall X Y: Prop, X /\ Y <-> forall Z: Prop, (X -> Y -> Z) -> Z. Proof. intros X Y. split. - intros [x y] Z f. exact (f x y). - intros f. exact (f (X /\ Y) (@conj X Y)). Qed. Goal forall X Y: Prop, X \/ Y <-> forall Z: Prop, (X -> Z) -> (Y -> Z) -> Z. Proof. intros X Y. split. - intros [x|y] Z f g. + exact (f x). + exact (g y). - intros f. exact (f (X \/ Y) (@or_introl X Y) (@or_intror X Y)). Show Proof. Qed. Goal forall X, forall Y, forall p: X -> Y -> Prop, (forall x, forall y, p x y) <-> (forall y, forall x: X, p x y). Proof. intros X Y p. split. - intros f y x. exact (f x y). - intros f x y. exact (f y x). Show Proof. Qed. Goal forall X (p: X -> Prop), ~ ~(forall x, p x) -> forall x, ~ ~p x. Proof. intros X p f x g. apply f. intros f'. exact (g (f' x)). Show Proof. Qed. Goal forall X (p q: X -> Prop), (forall x, p x <-> q x) -> (forall x, q x) -> forall x, p x. Proof. intros X p q f g x. destruct (f x) as [_ h]. exact (h (g x)). Show Proof. Qed. Goal forall X (p q: X -> Prop), (forall x, p x <-> q x) -> (forall x, q x) -> forall x, p x. Proof. intros X p q f g x. exact (proj2 (f x) (g x)). Qed. Goal forall X (x y: X), (forall p: X -> Prop, p x -> p y) -> (forall p: X -> Prop, p y -> p x). Proof. intros X x y f p. pattern y. apply f. exact (fun h => h). Show Proof. Qed. (** Tactics used: intros, apply, exact, split, destruct, pattern *)