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