intro f_readyForRupAdd
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ f.readyForRupAdd → (f.insert c).readyForRupAdd
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
⊢ (f.insert c).readyForRupAdd