(* Assignment 11, Exercise 11.2 *) Definition bot := forall Z :Prop, Z. Definition con (X Y :Prop) := forall Z :Prop, (X->Y->Z) -> Z. Definition dis (X Y :Prop) := forall Z :Prop, (X->Z) -> (Y->Z) -> Z. Definition ex (X :Type) (p :X->Prop) := forall Z :Prop, (forall x :X, p x -> Z) -> Z. (* a.i *) Proposition bot_False_equiv: bot <-> False. Proof. split. (* fill in your proof here *) Admitted. (* a.ii *) Proposition con_and_equiv: forall p q, con p q <-> p /\ q. Proof. split. (* fill in your proof here *) Admitted. (* a.iii *) Proposition dis_or_equiv: forall p q, dis p q <-> p \/ q. Proof. split. (* fill in your proof here *) Admitted. (* a.iv *) Proposition ex_exist_equiv: forall X (p :X->Prop), ex X p <-> exists x, (p x). Proof. split. (* fill in your proof here *) Admitted. (* b *) Proposition dis_intro_left: forall X Y :Prop, X -> dis X Y. Proof. (* fill in your proof here *) Admitted. Proposition dis_intro_right: forall X Y :Prop, Y -> dis X Y. Proof. (* fill in your proof here *) Admitted. Proposition dis_elim: forall X Y Z :Prop, dis X Y -> (X->Z) -> (Y->Z) -> Z. Proof. (* fill in your proof here *) Admitted.