cases b with
| inl =>
  exfalso
  dsimp [inj] at h
  have := lhs.isLt
  omega
| inr =>
  dsimp [inj] at h
  apply congrArg
  apply Fin.eq_of_val_eq
  exact h
case inr
aig : AIG Nat
b : aig.CNFVar
lhs : Fin aig.decls.size
h : inj (Sum.inr lhs) = inj b
⊢ Sum.inr lhs = b
no goals