apply Fin.eq_of_val_eq
case inr.inr.h
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ lhs = val✝
case inr.inr.h.a
aig : AIG Nat
lhs val✝ : Fin aig.decls.size
h : ↑lhs = ↑val✝
⊢ ↑lhs = ↑val✝