+(* Constructions with path_lcons ********************************************)
+
+lemma pcc_m_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐บโq) ฯต ๐โจnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐บ) โฆ Hq) -Hq
+/2 width=3 by pcc_m_dx/
+qed.
+
+lemma pcc_L_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐โq) ฯต ๐โจโnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐) โฆ Hq) -Hq
+/2 width=3 by pcc_L_dx/
+qed.
+
+lemma pcc_A_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐โq) ฯต ๐โจnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐) โฆ Hq) -Hq
+/2 width=3 by pcc_A_dx/
+qed.
+
+lemma pcc_S_sn (q) (n):
+ q ฯต ๐โจnโฉ โ (๐ฆโq) ฯต ๐โจnโฉ.
+#q #n #Hq
+lapply (pcc_append_bi (๐โ๐ฆ) โฆ Hq) -Hq
+/2 width=3 by pcc_S_dx/
+qed.
+