simpa using h
case mp.a
entry : Entrypoint Nat
assign1 : Nat → Bool
h :
  CNF.eval (toCNF.cnfSatAssignment entry.aig assign1)
      ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) =
    false
⊢ (⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign1⟧ &&
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.eval
        (toCNF.cnfSatAssignment entry.aig assign1)) =
    false
no goals