{α : Type u} →
  {motive : Std.Packages.PreorderOfLEArgs α → Sort u_1} →
    ((le : LE α) →
        (decidableLE : DecidableLE α) →
          (lt :
              let this := le;
              LT α) →
            (beq :
                let this := le;
                let this := decidableLE;
                BEq α) →
              (lt_iff :
                  let this := le;
                  let this_1 := lt;
                  ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) →
                (decidableLT :
                    let this := le;
                    let this := decidableLE;
                    let this := lt;
                    have this_1 := lt_iff;
                    DecidableLT α) →
                  (beq_iff_le_and_ge :
                      let this := le;
                      let this_1 := decidableLE;
                      let this_2 := beq;
                      ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a) →
                    (le_refl :
                        let this := le;
                        ∀ (a : α), a ≤ a) →
                      (le_trans :
                          let this := le;
                          ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c) →
                        motive
                          { le := le, decidableLE := decidableLE, lt := lt, beq := beq, lt_iff := lt_iff,
                            decidableLT := decidableLT, beq_iff_le_and_ge := beq_iff_le_and_ge, le_refl := le_refl,
                            le_trans := le_trans }) →
      (t : Std.Packages.PreorderOfLEArgs α) → motive t