example : False :=
  have : False := _

example : 5 = 3 :=
  have t : True := _
  have f : 5 = 6 := _
  f

example : True :=
  have := True.intro
  this