example (a b : Prop) : a ∧ b := begin apply or.inr end