-lemma lift_path_closed (f) (q) (n):
- q ϵ 𝐂❨n❩ → ↑[f]q ϵ 𝐂❨↑[q]f@❨n❩❩.
-#f #q #n #Hq elim Hq -Hq //
-#q #n [ #k ] #_ #IH
-/2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
+lemma lift_path_closed (o) (f) (q) (n):
+ q ϵ 𝐂❨o,n❩ → ↑[f]q ϵ 𝐂❨o,↑[q]f@❨n❩❩.
+#o #f #q #n #H0 elim H0 -q -n //
+#q #n [ #k #Ho ] #_ #IH
+/2 width=1 by pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
+/4 width=1 by pcc_d_dx, tr_xap_pos/