dsimp[verifyCert] at h1
c : CNF Nat
b : LratCert
h1 : verifyCert (LratFormula.ofCnf c) b = true
⊢ c.unsat
c : CNF Nat
b : LratCert
h1 :
  (match LRAT.parseLRATProof (String.toUTF8 b) with
    | some lratProof =>
      decide
        (LRAT.lratChecker (LratFormula.ofCnf c).formula
            (List.map Subtype.val
              (List.filterMap
                (fun actOpt =>
                  match actOpt with
                  | none => none
                  | some (LRAT.Action.addEmpty id rupHints) => some ⟨LRAT.Action.addEmpty id rupHints, True.intro⟩
                  | some (LRAT.Action.addRup id c_1 rupHints) => some ⟨LRAT.Action.addRup id c_1 rupHints, True.intro⟩
                  | some (LRAT.Action.del ids) => some ⟨LRAT.Action.del ids, True.intro⟩
                  | some (LRAT.Action.addRat id c_1 pivot rupHints ratHints) =>
                    if h : pivot ∈ LRAT.Clause.toList c_1 then
                      some ⟨LRAT.Action.addRat id c_1 pivot rupHints ratHints, ⋯⟩
                    else none)
                (List.map (LRAT.intActionToDefaultClauseAction ((LratFormula.ofCnf c).numVars + 1))
                  lratProof.toList))) =
          LRAT.Result.success)
    | none => false) =
    true
⊢ c.unsat