theorem ex : let x := 1; x < 2 := by
  intro x
  decide