simp[h]
X : Type
inst✝⁹ : NormedAddCommGroup X
inst✝⁸ : NormedSpace ℝ X
inst✝⁷ : MeasurableSpace X
Y : Type
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace ℝ Y
inst✝⁴ : MeasurableSpace Y
Z : Type ?u.2238
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ Z
inst✝¹ : MeasurableSpace Z
c : Prop
inst✝ : Decidable c
t f : FDRand X
φ : X → Y
h : c
⊢ FDRand.fdE (if c then t else f) φ = if c then FDRand.fdE t φ else FDRand.fdE f φ
no goals