Cost query

@[simp] lemma cost_query' {i : I} (m : i ∈ s) {n : ℕ} (y : Vector Bool n) (f0 f1 : Comp s α)    (o : I → Oracle) (j : I) :    (Comp.query' i m n y f0 f1).cost o j =      (if j = i then 1 else 0) +      (o i _ y).exp (fun x ↦ if x then f0.cost o j else f1.cost o j) := by  simp only [cost, run, exp_bind, Nat.cast_zero]  rw [←exp_const_add]; apply exp_congr; intro x _; induction x;  repeat simp only [ite_false, ite_true, exp_bind, exp_pure, Pi.add_apply, Nat.cast_add,    Nat.cast_ite, Nat.cast_one, Nat.cast_zero, exp_add, exp_const, add_comm]