rw [BoolExpr.eval_congr, eval_if f, BoolExpr.eval_congr, eval_if f]
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ g.eval (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) x.toBoolExpr)
      (BoolExpr.eval (fun i => decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) y.toBoolExpr) =
    g.eval (eval f x) (eval f y)
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < y.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < y.toBoolExpr.vars) && f.getD i false)

case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
⊢ ∀ (i : Nat),
    i < x.toBoolExpr.vars →
      (decide (i < max x.toBoolExpr.vars y.toBoolExpr.vars) && f.getD i false) =
        (decide (i < x.toBoolExpr.vars) && f.getD i false)