proposition: Lemma or20_equiv: forall A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 A12 A13 A14 A15 A16 A17 A18 A19 A20 , or20 A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 A12 A13 A14 A15 A16 A17 A18 A19 A20 <-> A1 \/ A2 \/ A3 \/ A4 \/ A5 \/ A6 \/ A7 \/ A8 \/ A9 \/ A10 \/ A11 \/ A12 \/ A13 \/ A14 \/ A15 \/ A16 \/ A17 \/ A18 \/ A19 \/ A20 .
proof: Proof. intros. split. intros H. rewrite <- or19_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. exact H. constructor 10. exact H. constructor 11. exact H. constructor 12. exact H. constructor 13. exact H. constructor 14. exact H. constructor 15. exact H. constructor 16. exact H. constructor 17. exact H. constructor 18. exact H. constructor 19. left. exact H. constructor 19. right. exact H. intros H. destruct H. constructor 1. exact H. rewrite <- or19_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. constructor 11. exact H. constructor 12. exact H. constructor 13. exact H. constructor 14. exact H. constructor 15. exact H. constructor 16. exact H. constructor 17. exact H. constructor 18. exact H. constructor 19. exact H. constructor 20. exact H. Qed.
imports: Coq(Setoid Morphisms)