variables A B : Prop example : A ∧ ¬B → ¬B ∧ A := assume h : A ∧ ¬B, and.intro (and.right h) (and.left h)