variables p q : Prop example (hp : p) (hq : q) : p ∧ q := and.intro hp hq -- 1ª demostración (Con constructores) example (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩