example : True := True.intro

example : False := sorry


-- Let p be any proposition.

-- ¬q written as an implication: q → False
example : (p : Prop) → ¬(p ∧ (¬p)) := fun p =>
  fun ⟨ a, b ⟩ => b a

example : ((p → False) → False) → p := fun f => f sorry