Theorem: CNF.convertLRAT_readfyForRupAdd (LeanSAT/Reflect/Glue.lean)

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

State before:
cnf : CNF Nat
⊢ (let lifted := cnf.lift;
    let lratCnf := lifted.convertLRAT';
    LRAT.DefaultFormula.ofArray (List.toArray (none :: lratCnf))).readyForRupAdd
Tactic:
apply LRAT.DefaultFormula.ofArray_readyForRupAdd
State after:
no goals