simp_all
case h_1
α : 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
hidx1 : decls2[start] = decls1[start]
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
hidx2 : decls2[lhs] = decls1[lhs]
hidx3 : decls2[rhs] = decls1[rhs]
b✝ : Bool
heq✝ : decls1[start] = Decl.const b✝
⊢ (let_fun this := ⋯;
    let lval := go lhs decls2 assign ⋯ hdag2;
    let rval := go rhs decls2 assign ⋯ hdag2;
    xor lval linv && xor rval rinv) =
    b✝
no goals