∀ {s : String},
  let this := inferInstance;
  let this_1 := inferInstance;
  let this_2 :=
    let this := inferInstance;
    let this_2 := inferInstance;
    Max.leftLeaningOfLE s.Pos;
  ∀ (a b : s.Pos), a ⊔ b = if b ≤ a then a else b