. intro a b _ _ hinj
  apply toCNF.inj_is_injection
  assumption
entry : Entrypoint Nat
⊢ ∀ {a b : entry.aig.CNFVar},
    CNF.mem a
        ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
          (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
      CNF.mem b
          ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
            (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf) →
        toCNF.inj a = toCNF.inj b → a = b
no goals