rw [c'_eq_c]
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c