unfold CNF.convertLRAT
cnf : CNF Nat
⊢ cnf.convertLRAT.readyForRupAdd
cnf : CNF Nat
⊢ (let lifted := cnf.lift;
    let lratCnf := lifted.convertLRAT';
    LRAT.DefaultFormula.ofArray (List.toArray (none :: lratCnf))).readyForRupAdd