proposition: Lemma or2_equiv: forall A1 A2 , or2 A1 A2 <-> A1 \/ A2 .
proof: Proof. intros. split. intros H. destruct H. left. assumption. right. assumption. intros H. destruct H. constructor 1. exact H. constructor 2. exact H. Qed.
imports: Coq(Setoid Morphisms)