. simp only [insert, h.1] <;> split <;> rfl
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).ratUnits = #[]

case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRupAdd
case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRupAdd