simp [eval, ihx, ihy, toBoolExpr]
case gate
f : List Bool
g : Gate
x y : BoolExprNat
ihx : BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
ihy : BoolExpr.eval (fun x => f.getD x false) y.toBoolExpr = eval f y
⊢ BoolExpr.eval (fun x => f.getD x false) (gate g x y).toBoolExpr = eval f (gate g x y)
no goals