--
-- 5. Tactics
--

--
theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := by
  apply And.intro
  exact hp
  exact { left := hq, right := hp }