9 lines
155 B
Text
9 lines
155 B
Text
--
|
|
-- 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 }
|