{α : Type u} →
  {motive : Std.Packages.LinearOrderOfLEArgs α → Sort u_1} →
    (t : Std.Packages.LinearOrderOfLEArgs α) →
      ((toLinearPreorderOfLEArgs : Std.Packages.LinearPreorderOfLEArgs α) →
          (le_antisymm :
              let this := toLinearPreorderOfLEArgs.le;
              ∀ (a b : α), a ≤ b → b ≤ a → a = b) →
            (min :
                let this := toLinearPreorderOfLEArgs.le;
                let this := toLinearPreorderOfLEArgs.decidableLE;
                Min α) →
              (max :
                  let this := toLinearPreorderOfLEArgs.le;
                  let this := toLinearPreorderOfLEArgs.decidableLE;
                  Max α) →
                (min_eq :
                    let this := toLinearPreorderOfLEArgs.le;
                    let this_1 := toLinearPreorderOfLEArgs.decidableLE;
                    let this_2 := min;
                    ∀ (a b : α), a ⊓ b = if a ≤ b then a else b) →
                  (max_eq :
                      let this := toLinearPreorderOfLEArgs.le;
                      let this_1 := toLinearPreorderOfLEArgs.decidableLE;
                      let this_2 := max;
                      ∀ (a b : α), a ⊔ b = if b ≤ a then a else b) →
                    motive
                      { toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs, le_antisymm := le_antisymm, min := min,
                        max := max, min_eq := min_eq, max_eq := max_eq }) →
        motive t