variables A B : Prop section variables (h1 : A) (h2 : B) example : A ∧ B := and.intro h1 h2 end section variable h : A ∧ B example : A := and.left h example : B := and.right h end