apply denote.go_eq_of_aig_eq
case h_3.e_y.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ go rhs decls2 assign ⋯ hdag2 = go rhs decls1 assign ⋯ hdag1
case h_3.e_y.e_a.hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
lhs rhs : Nat
linv rinv : Bool
heq✝² : decls2[start] = Decl.gate lhs rhs linv rinv
heq✝¹ : decls1[start] = Decl.gate lhs rhs linv rinv
foo : lhs < start ∧ rhs < start
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls1[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : lidx✝ = lhs ∧ ridx✝ = rhs ∧ linv✝ = linv ∧ rinv✝ = rinv
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
⊢ IsPrefix decls1 decls2