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