rw [denote_idx_gate heq2]
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
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    ⟦{ 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
heq1 : (relabel f aig).decls[start] = Decl.gate lhs rhs linv rinv
heq2 : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (xor ⟦{ aig := relabel f aig, ref := { gate := lhs, hgate := ⋯ } }, assign⟧ linv &&
      xor ⟦{ aig := relabel f aig, ref := { gate := rhs, hgate := ⋯ } }, assign⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign ∘ f⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign ∘ f⟧ rinv)