∀ (α : Type u_3) (β : Type u_2) (γ : Type u_1) [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ]
  (motive : (a b : Lex (Lex (α ⊕ β) ⊕ γ)) → (Equiv.sumAssoc α β γ) a ≤ (Equiv.sumAssoc α β γ) b → Prop)
  (a b : Lex (Lex (α ⊕ β) ⊕ γ)) (h : (Equiv.sumAssoc α β γ) a ≤ (Equiv.sumAssoc α β γ) b),
  (∀ (val val_1 : α) (h : val ≤ val_1), motive (Sum.inl (Sum.inl val)) (Sum.inl (Sum.inl val_1)) ⋯) →
    (∀ (val : α) (val_1 : β), motive (Sum.inl (Sum.inl val)) (Sum.inl (Sum.inr val_1)) ⋯) →
      (∀ (val : α) (val_1 : γ), motive (Sum.inl (Sum.inl val)) (Sum.inr val_1) ⋯) →
        (∀ (val val_1 : β) (h : val ≤ val_1), motive (Sum.inl (Sum.inr val)) (Sum.inl (Sum.inr val_1)) ⋯) →
          (∀ (val : β) (val_1 : γ), motive (Sum.inl (Sum.inr val)) (Sum.inr val_1) ⋯) →
            (∀ (val val_1 : γ) (h : val ≤ val_1), motive (Sum.inr val) (Sum.inr val_1) ⋯) → motive a b h