cases b with
| inl =>
  dsimp [inj] at h
  apply congrArg
  apply Nat.add_left_cancel
  exact h
| inr rhs =>
  exfalso
  dsimp [inj] at h
  have := rhs.isLt
  omega
case inl
aig : AIG Nat
b : aig.CNFVar
val✝ : Nat
h : inj (Sum.inl val✝) = inj b
⊢ Sum.inl val✝ = b
no goals