q Ļµ šāØnā© ā ā[ā[p]f]q Ļµ šāØā[pāq]fļ¼ āØnā©ā©.
/2 width=1 by lift_path_closed/
qed.
+
+lemma lift_path_rmap_closed_L (f) (p) (q) (n):
+ q Ļµ šāØnā© ā ā[ā[pāš]f]q Ļµ šāØā[pāšāq]fļ¼ Ā§āØnā©ā©.
+#f #p #q #n #Hq
+lapply (lift_path_closed (ā[pāš]f) ā¦ Hq) #Hq0
+lapply (pcc_L_sn ā¦ Hq) -Hq #Hq1
+lapply (lift_path_rmap_closed f p ā¦ Hq1) -Hq1
+<lift_path_L_sn >lift_rmap_L_dx #Hq1
+elim (pcc_inv_L_sn ā¦ Hq1 Hq0) -Hq1 #H0 #_
+<H0 in Hq0; -H0 //
+qed.