-- Lean 4's syntax makes this quite nice...

def t2 : Option Bool :=
  let x := 42
  let y := 41
  if x > y then some true else none

-- Lift any local assignments and compile the rest to an ITE?