. contradiction
case h_1
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
b✝ : Bool
heq✝ : decls[idx] = const b✝
h : const b✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_2
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (f a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x
case h_2
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
a✝ : α
heq✝ : decls[idx] = atom a✝
h : atom (f a✝) = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x

case h_3
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
decl✝ : Decl α
lhs✝ rhs✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls[idx] = gate lhs✝ rhs✝ linv✝ rinv✝
h : gate lhs✝ rhs✝ linv✝ rinv✝ = atom a
⊢ ∃ x, decls[idx] = atom x ∧ a = f x