proposition: Lemma or7_equiv: forall A1 A2 A3 A4 A5 A6 A7 , or7 A1 A2 A3 A4 A5 A6 A7 <-> A1 \/ A2 \/ A3 \/ A4 \/ A5 \/ A6 \/ A7 .
proof: Proof. intros. split. intros H. rewrite <- or6_equiv. destruct H. constructor 1. exact H. constructor 2. exact H. constructor 3. exact H. constructor 4. exact H. constructor 5. exact H. constructor 6. left. exact H. constructor 6. right. exact H. intros H. destruct H. constructor 1. exact H. rewrite <- or6_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. constructor 7. exact H. Qed.
imports: Coq(Setoid Morphisms)