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

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

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