proposition: Lemma or10_equiv: forall A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 , or10 A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 <-> A1 \/ A2 \/ A3 \/ A4 \/ A5 \/ A6 \/ A7 \/ A8 \/ A9 \/ A10 .
proof: Proof. intros. split. intros H. rewrite <- or9_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. exact H. constructor 7. exact H. constructor 8. exact H. constructor 9. left. exact H. constructor 9. right. exact H. intros H. destruct H. constructor 1. exact H. rewrite <- or9_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. constructor 8. exact H. constructor 9. exact H. constructor 10. exact H. Qed.
imports: Coq(Setoid Morphisms)