matita/matita/contribs/lambdadelta/delayed_updating/etc/path_proper.etc

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