apply congrArg
case inl.inl
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ Sum.inl val✝¹ = Sum.inl val✝
case inl.inl.h
aig : AIG Nat
val✝¹ val✝ : Nat
h : aig.decls.size + val✝¹ = aig.decls.size + val✝
⊢ val✝¹ = val✝