--- /dev/null
+include "delayed_updating/unwind/unwind2_rmap_closed.ma".
+
+lemma pippo (o) (q) (n):
+ (q◖𝗟) ϵ 𝐂❨o,n❩ →
+ (𝗟◗q) ϵ 𝐂❨o,n❩.
+#o #q elim q -q //
+* [ #k ] #q #IH #n #H0
+elim (pcc_inv_L_dx … H0) -H0 #H0 #Hn
+[ elim (pcc_inv_d_dx … H0) -H0 #_ #H0
+ >Hn -Hn /4 width=1 by pcc_d_dx, pcc_L_dx/
+| lapply (pcc_inv_m_dx … H0) -H0 #H0
+ >Hn -Hn /4 width=1 by pcc_m_dx, pcc_L_dx/
+| elim (pcc_inv_L_dx … H0) -H0 #H0 #Hnn
+ >Hn -Hn /4 width=1 by pcc_L_dx/
+| lapply (pcc_inv_A_dx … H0) -H0 #H0
+ >Hn -Hn /4 width=1 by pcc_A_dx, pcc_L_dx/
+| lapply (pcc_inv_S_dx … H0) -H0 #H0
+ >Hn -Hn /4 width=1 by pcc_S_dx, pcc_L_dx/
+]
+qed-.
+
+
+lemma pippo (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ → ♭q < ▶[f]q@⧣❨↑n❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <depth_d_dx <unwind2_rmap_d_dx
+ <tr_compose_pap <tr_uni_pap //
+| <depth_L_dx <unwind2_rmap_L_dx
+ <tr_pap_push
+ /2 width=1 by nlt_succ_bi/
+]
+qed-.
+
+lemma pippo2 (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ → ▶[f]q@❨n❩ ≤ ♭q.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+ @(nle_trans … IH) -IH
+ <tr_compose_xap
+| <unwind2_rmap_L_dx <depth_L_dx
+ <tr_xap_push
+ /2 width=1 by nle_succ_bi/
+]
+qed-.
+
+lemma pippo (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ → n < ▶[f]q@⧣❨↑♭q❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <unwind2_rmap_d_dx <depth_d_dx
+ <tr_compose_pap <tr_uni_pap
+ @(nlt_trans … (n+k)) [ // ]
+ @(nlt_trans … IH) -IH
+| <unwind2_rmap_L_dx <depth_L_dx <tr_pap_push
+ /2 width=1 by nlt_succ_bi/