match x with
| .literal i => dsimp [eval]; apply w; simp
| .const b => rfl
| .not x =>
  dsimp [eval]
  rw [eval_congr f g]
  exact w
| .gate h x y =>
  dsimp [eval]
  rw [eval_congr f g, eval_congr f g]
  exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_right _ _))
  exact fun i h => w i (Nat.lt_of_lt_of_le h (Nat.le_max_left _ _))
x : BoolExpr Nat
f g : Nat → Bool
w : ∀ (i : Nat), i < x.vars → f i = g i
⊢ eval f x = eval g x
no goals