dsimp [inj] at h
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : inj (Sum.inr lhs) = inj (Sum.inl val✝)
⊢ False
case inr.inl
aig : AIG Nat
lhs : Fin aig.decls.size
val✝ : Nat
h : ↑lhs = aig.decls.size + val✝
⊢ False