{motive_1 : Lean.Meta.Grind.AC.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.AC.EqCnstrProof → Sort u} →
    ((lhs rhs : Lean.Grind.AC.Seq) →
        (h : Lean.Meta.Grind.AC.EqCnstrProof) →
          (id : ℕ) → motive_2 h → motive_1 { lhs := lhs, rhs := rhs, h := h, id := id }) →
      ((a b : Lean.Expr) → (ea eb : Lean.Grind.AC.Expr) → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.core a b ea eb)) →
        ((c : Lean.Meta.Grind.AC.EqCnstr) → motive_1 c → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.erase_dup c)) →
          ((c : Lean.Meta.Grind.AC.EqCnstr) → motive_1 c → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.erase0 c)) →
            ((c : Lean.Meta.Grind.AC.EqCnstr) → motive_1 c → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.swap c)) →
              ((lhs : Bool) →
                  (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) →
                    motive_1 c₁ → motive_1 c₂ → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.simp_exact lhs c₁ c₂)) →
                ((lhs : Bool) →
                    (s : Lean.Grind.AC.Seq) →
                      (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) →
                        motive_1 c₁ → motive_1 c₂ → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.simp_ac lhs s c₁ c₂)) →
                  ((lhs : Bool) →
                      (s : Lean.Grind.AC.Seq) →
                        (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) →
                          motive_1 c₁ →
                            motive_1 c₂ → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.simp_suffix lhs s c₁ c₂)) →
                    ((lhs : Bool) →
                        (s : Lean.Grind.AC.Seq) →
                          (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) →
                            motive_1 c₁ →
                              motive_1 c₂ → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.simp_prefix lhs s c₁ c₂)) →
                      ((lhs : Bool) →
                          (s₁ s₂ : Lean.Grind.AC.Seq) →
                            (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) →
                              motive_1 c₁ →
                                motive_1 c₂ → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.simp_middle lhs s₁ s₂ c₁ c₂)) →
                        ((r₁ c r₂ : Lean.Grind.AC.Seq) →
                            (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) →
                              motive_1 c₁ →
                                motive_1 c₂ → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac r₁ c r₂ c₁ c₂)) →
                          ((p s c : Lean.Grind.AC.Seq) →
                              (c₁ c₂ : Lean.Meta.Grind.AC.EqCnstr) →
                                motive_1 c₁ →
                                  motive_1 c₂ → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.superpose p s c c₁ c₂)) →
                            ((x : Lean.Grind.AC.Var) →
                                (c₁ : Lean.Meta.Grind.AC.EqCnstr) →
                                  motive_1 c₁ →
                                    motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.superpose_ac_idempotent x c₁)) →
                              ((x : Lean.Grind.AC.Var) →
                                  (c₁ : Lean.Meta.Grind.AC.EqCnstr) →
                                    motive_1 c₁ →
                                      motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.superpose_head_idempotent x c₁)) →
                                ((x : Lean.Grind.AC.Var) →
                                    (c₁ : Lean.Meta.Grind.AC.EqCnstr) →
                                      motive_1 c₁ →
                                        motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent x c₁)) →
                                  ((s : Lean.Grind.AC.Seq) → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.refl s)) →
                                    ((c : Lean.Meta.Grind.AC.EqCnstr) →
                                        motive_1 c → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.erase_dup_rhs c)) →
                                      ((c : Lean.Meta.Grind.AC.EqCnstr) →
                                          motive_1 c → motive_2 (Lean.Meta.Grind.AC.EqCnstrProof.erase0_rhs c)) →
                                        (t : Lean.Meta.Grind.AC.EqCnstrProof) → motive_2 t