Section Ex20080108. Hypothesis A : Prop. Hypotheses B C : Prop. Theorem andComm : A /\ B -> B /\ A. intros h. inversion_clear h as [ a b ]. split. assumption. exact a. Qed. Print andComm. Theorem impI : (not A \/ B) -> (A -> B). intros h a. inversion_clear h as [ na | b ]. cut False. intro c. inversion c. (* contradiction. *) apply na. assumption. assumption. Qed. Theorem impI' : (not A \/ B) -> (A -> B). intros h a. inversion_clear h as [ na | b ]. contradiction. assumption. Qed. Definition orComm : A \/ B -> B \/ A := fun h => match h with | or_introl x => or_intror B x | or_intror x => or_introl A x end. Definition orComm' (h : A \/ B) : B \/ A := match h with | or_introl x => or_intror _ x | or_intror x => or_introl _ x end. Definition myfun (x y : nat) : nat := x + y. End Ex20080108.