proposition: Lemma or6_equiv: forall A1 A2 A3 A4 A5 A6 , or6 A1 A2 A3 A4 A5 A6 <-> A1 \/ A2 \/ A3 \/ A4 \/ A5 \/ A6 .
proof: Proof. intros. split. intros H. rewrite <- or5_equiv. destruct H. constructor 1. exact H. constructor 2. exact H. constructor 3. exact H. constructor 4. exact H. constructor 5. left. exact H. constructor 5. right. exact H. intros H. destruct H. constructor 1. exact H. rewrite <- or5_equiv in H. destruct H. constructor 2. exact H. constructor 3. exact H. constructor 4. exact H. constructor 5. exact H. constructor 6. exact H. Qed.
imports: Coq(Setoid Morphisms)