rw [eval_congr f g, eval_congr f g]
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ h.eval (eval f x) (eval f y) = h.eval (eval g x) (eval g y)
x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < y.vars → f i = g i

x✝ : BoolExpr Nat
f g : Nat → Bool
h : Gate
x y : BoolExpr Nat
w : ∀ (i : Nat), i < (gate h x y).vars → f i = g i
⊢ ∀ (i : Nat), i < x.vars → f i = g i