next heq =>
rw [mkAtom, Array.get_push_size] at heq
contradiction
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
var : α
assign : α → Bool
aig : AIG α
b✝ : Bool
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.const b✝
⊢ b✝ = assign var
no goals