∀ {s : String},
  let this := inferInstance;
  let this_1 := inferInstance;
  let this_2 :=
    let this := inferInstance;
    let this_2 := inferInstance;
    Std.FactoryInstances.instOrdOfDecidableLE;
  ∀ (a b : s.Pos), (compare a b).isLE = true ↔ a ≤ b