-theorem pcc_append_bi (p) (q) (m) (n):
- p ฯต ๐โจmโฉ โ q ฯต ๐โจnโฉ โ pโq ฯต ๐โจm+nโฉ.
-#p #q #m #n #Hm #Hm elim Hm -Hm // -Hm
-#p #n [ #k ] #_ #IH [3: <nplus_succ_dx ]
-/2 width=1 by pcc_d_dx, pcc_m_dx, pcc_L_dx, pcc_A_dx, pcc_S_dx/
+theorem pcc_append_bi (o1) (o2) (p) (q) (m) (n):
+ p ฯต ๐โจo1,mโฉ โ q ฯต ๐โจo2,nโฉ โ pโq ฯต ๐โจo1โงo2,m+nโฉ.
+#o1 #o2 #p #q #m #n #Hm #Hn elim Hn -q -n
+/2 width=1 by pcc_m_dx, pcc_A_dx, pcc_S_dx, pcc_land_dx/
+#q #n [ #k #Ho2 ] #_ #IH
+[ @pcc_d_dx // #H0
+ elim (andb_inv_true_sn โฆ H0) -H0 #_ #H0 >Ho2 //
+ <nplus_succ_dx <npred_succ //
+| <nplus_succ_dx /2 width=1 by pcc_L_dx/
+]
+qed.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma pcc_m_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐บโq) ฯต ๐โจo,nโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐บ) โฆ Hq) -Hq
+/2 width=3 by pcc_m_dx/
+qed.
+
+lemma pcc_L_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐โq) ฯต ๐โจo,โnโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐) โฆ Hq) -Hq
+/2 width=3 by pcc_L_dx/
+qed.
+
+lemma pcc_A_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐โq) ฯต ๐โจo,nโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐) โฆ Hq) -Hq
+/2 width=3 by pcc_A_dx/
+qed.
+
+lemma pcc_S_sn (o) (q) (n):
+ q ฯต ๐โจo,nโฉ โ (๐ฆโq) ฯต ๐โจo,nโฉ.
+#o #q #n #Hq
+lapply (pcc_append_bi (โ) โฆ (๐โ๐ฆ) โฆ Hq) -Hq
+/2 width=3 by pcc_S_dx/