theorem and_swap_demo (P Q : Prop) : P ∧ Q → Q ∧ P := fun h => ⟨h.2, h.1⟩