simp only [h, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp, decide_eq_true_eq]
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : 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
h : i < y.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars