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