(* Main constructions with tr_compose and tr_tls ****************************)
-theorem tr_compose_uni_dx (f) (p):
- (𝐮❨f@❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
+theorem tr_compose_uni_dx_pap (f) (p):
+ (𝐮❨f@⧣❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
#f #p
@nstream_eq_inv_ext #q
<tr_compose_pap <tr_compose_pap