intro h
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ f.readyForRatAdd → (f.insert c).readyForRatAdd
n : Nat
f : DefaultFormula n
c : DefaultClause n
h : f.readyForRatAdd
⊢ (f.insert c).readyForRatAdd