. intro a heq1
  rw [denote_idx_atom heq1]
  rcases relabel_atom heq1 with ⟨x, ⟨hlx, hrx⟩⟩
  rw [hrx] at heq1
  rw [denote_idx_atom hlx]
  simp [hrx]
case hatom
α : 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 : β),
    (relabel f aig).decls[start] = Decl.atom a →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧

case hgate
α : 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
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧
case hgate
α : 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
⊢ ∀ (lhs rhs : Nat) (linv rinv : Bool),
    (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv →
      ⟦{ aig := relabel f aig, ref := { gate := start, hgate := hidx } }, assign⟧ =
        ⟦{ aig := aig, ref := { gate := start, hgate := ⋯ } }, assign ∘ f⟧