sorry_proof
R : Type u_1
inst✝¹⁰ : RealScalar R
X : Type u_2
inst✝⁹ : Vec R X
Y : Type u_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
U : Type u_3
inst✝⁵ : Vec R U
inst✝⁴ : Module ℝ U
V : Type ?u.22929
inst✝³ : Vec R V
inst✝² : Module ℝ V
W : Type ?u.23786
inst✝¹ : Vec R W
inst✝ : Module ℝ W
x : 𝒟'(X, U)
y : U ⊸[R] 𝒟'(Y, Z)
φ : Y → R
⊢ Distribution.postComp (Distribution.postComp x y) (fun T ⊸ Distribution.extAction' T φ) =
    Distribution.postComp x (fun u ⊸ Distribution.extAction' (y u) φ)
no goals