simp [hrx]
case hatom.intro.intro
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
aig : AIG α
f : α → β
start : Nat
hidx : start < (relabel f aig).decls.size
assign : β → Bool
a : β
x : α
heq1 : (relabel f aig).decls[start] = Decl.atom (f x)
hlx : aig.decls[start] = Decl.atom x
hrx : a = f x
⊢ assign a = (assign ∘ f) x
no goals