next heq =>
rw [mkConst, Array.get_push_size] at heq
contradiction
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
assign : α → Bool
aig : AIG α
idx✝ : α
heq✝ : (aig.mkConst val).aig.decls[(aig.mkConst val).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = val
no goals