{motive : Mathlib.Tactic.Sat.LRATStep → Sort u} →
  ((id : ℕ) → (lits proof : Array ℤ) → motive (Mathlib.Tactic.Sat.LRATStep.add id lits proof)) →
    ((ids : Array ℕ) → motive (Mathlib.Tactic.Sat.LRATStep.del ids)) → (t : Mathlib.Tactic.Sat.LRATStep) → motive t