have := aig.inv upper lhs rhs linv rinv h heq
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
⊢ lhs < aig.decls.size
upper lhs rhs : Nat
linv rinv : Bool
aig : AIG Nat
h : upper < aig.decls.size
heq : aig.decls[upper] = Decl.gate lhs rhs linv rinv
this : lhs < upper ∧ rhs < upper
⊢ lhs < aig.decls.size