(motive : Mathlib.Tactic.Order.AtomicFact → Sort u_1) →
  (fa : Mathlib.Tactic.Order.AtomicFact) →
    ((lhs rhs : ℕ) → (proof : Lean.Expr) → motive (Mathlib.Tactic.Order.AtomicFact.eq lhs rhs proof)) →
      ((lhs rhs : ℕ) → (proof : Lean.Expr) → motive (Mathlib.Tactic.Order.AtomicFact.ne lhs rhs proof)) →
        ((lhs rhs : ℕ) → (proof : Lean.Expr) → motive (Mathlib.Tactic.Order.AtomicFact.le lhs rhs proof)) →
          ((lhs rhs : ℕ) → (proof : Lean.Expr) → motive (Mathlib.Tactic.Order.AtomicFact.nle lhs rhs proof)) →
            ((lhs rhs : ℕ) → (proof : Lean.Expr) → motive (Mathlib.Tactic.Order.AtomicFact.lt lhs rhs proof)) →
              ((lhs rhs : ℕ) → (proof : Lean.Expr) → motive (Mathlib.Tactic.Order.AtomicFact.nlt lhs rhs proof)) →
                ((idx : ℕ) → motive (Mathlib.Tactic.Order.AtomicFact.isTop idx)) →
                  ((idx : ℕ) → motive (Mathlib.Tactic.Order.AtomicFact.isBot idx)) →
                    ((lhs rhs res : ℕ) → motive (Mathlib.Tactic.Order.AtomicFact.isInf lhs rhs res)) →
                      ((lhs rhs res : ℕ) → motive (Mathlib.Tactic.Order.AtomicFact.isSup lhs rhs res)) → motive fa