∀ (α : Type u_3) (β : Type u_2) (γ : Type u_1) [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {a b : Lex (Lex (α × β) × γ)},
  (ofLex
            (toLex
              (Prod.map ⇑(Equiv.refl α) ⇑toLex
                ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                  (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                  (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).1 <
        (ofLex
            (toLex
              (Prod.map ⇑(Equiv.refl α) ⇑toLex
                ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                  (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                  (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).1 ∨
      (ofLex
              (toLex
                (Prod.map ⇑(Equiv.refl α) ⇑toLex
                  ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                    (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                    (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).1 =
          (ofLex
              (toLex
                (Prod.map ⇑(Equiv.refl α) ⇑toLex
                  ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                    (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                    (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).1 ∧
        ((ofLex
                (ofLex
                    (toLex
                      (Prod.map ⇑(Equiv.refl α) ⇑toLex
                        ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                          (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                          (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).2).1 <
            (ofLex
                (ofLex
                    (toLex
                      (Prod.map ⇑(Equiv.refl α) ⇑toLex
                        ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                          (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                          (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).2).1 ∨
          (ofLex
                  (ofLex
                      (toLex
                        (Prod.map ⇑(Equiv.refl α) ⇑toLex
                          ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).2).1 =
              (ofLex
                  (ofLex
                      (toLex
                        (Prod.map ⇑(Equiv.refl α) ⇑toLex
                          ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).2).1 ∧
            (ofLex
                  (ofLex
                      (toLex
                        (Prod.map ⇑(Equiv.refl α) ⇑toLex
                          ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.1,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).1.2,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex a)).2)))).2).2 ≤
              (ofLex
                  (ofLex
                      (toLex
                        (Prod.map ⇑(Equiv.refl α) ⇑toLex
                          ((Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.1,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).1.2,
                            (Prod.map (⇑ofLex) (⇑(Equiv.refl γ)) (ofLex b)).2)))).2).2) ↔
    ((ofLex (ofLex a).1).1 < (ofLex (ofLex b).1).1 ∨
        (ofLex (ofLex a).1).1 = (ofLex (ofLex b).1).1 ∧ (ofLex (ofLex a).1).2 < (ofLex (ofLex b).1).2) ∨
      (ofLex a).1 = (ofLex b).1 ∧ (ofLex a).2 ≤ (ofLex b).2