1 (* Constructions with path_append *******************************************)
3 lemma ppc_append_sn (p2) (p1): Ꝕp2 → Ꝕ(p1●p2).
4 #p2 * /2 width=3 by ppc_lcons/
7 lemma ppc_append_dx (p1) (p2): Ꝕp1 → Ꝕ(p1●p2).
9 elim (ppc_inv_lcons … Hp1) -Hp1 #l #q1 #H destruct
10 /2 width=3 by ppc_lcons/
13 (* Constructions with path_rcons ********************************************)
15 lemma ppc_rcons (q) (l): Ꝕ(q◖l).
16 /2 width=1 by ppc_lcons, ppc_append_sn/