. simp only [decide_eq_true_eq] at h1
  have h2 :=
    lratCheckerSound
      _
      (by apply CNF.convertLRAT_readfyForRupAdd)
      (by apply CNF.convertLRAT_readfyForRatAdd)
      _
      (by
        intro action h
        simp only [List.mem_map, List.mem_filterMap] at h
        rcases h with ⟨wellFormedActions, _, h2⟩
        rw [← h2]
        exact wellFormedActions.property)
      h1
  apply CNF.unsat_of_lift_unsat c
  intro assignment
  unfold CNF.convertLRAT at h2
  have h2 := (LRAT.unsat_of_cons_none_unsat _ h2) assignment
  apply eq_false_of_ne_true
  intro h3
  apply h2
  simp only [LRAT.Formula.formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
  intro lratClause hlclause
  simp only [LRAT.Formula.toList, LRAT.DefaultFormula.toList, LRAT.DefaultFormula.ofArray,
    CNF.convertLRAT', Array.size_toArray, List.length_map, Array.toList_eq, Array.data_toArray,
    List.map_nil, List.append_nil, List.mem_filterMap, List.mem_map, id_eq, exists_eq_right] at hlclause
  rcases hlclause with ⟨reflectClause, ⟨hrclause1, hrclause2⟩⟩
  simp only [CNF.eval, List.all_eq_true] at h3
  split at hrclause2
  . next heq =>
    rw [← heq] at hrclause2
    simp only [Option.some.injEq] at hrclause2
    simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h3 reflectClause hrclause1]
  . contradiction
case h_1
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
lratProof✝ : Array LRAT.IntAction
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = some lratProof✝
h1 :
  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) =
    true
⊢ c.unsat

case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat
case h_2
c : CNF Nat
b : LratCert
x✝ : Option (Array LRAT.IntAction)
heq✝ : LRAT.parseLRATProof (String.toUTF8 b) = none
h1 : false = true
⊢ c.unsat