. assumption
case intro.mk.a
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.decls[?intro.mk.idx] = Decl.atom a

case intro.mk.decls
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Array (Decl α)

case intro.mk.idx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 ?intro.mk.decls ?intro.mk.upper (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.idx < ?intro.mk.upper
case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls ?intro.mk.upper (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < ?intro.mk.upper