partial commit in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / path_inner.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
index 98501e8df7a59131f8b31a6002021604b4899db3..0db6d2f65327310a9a7d5d6ba2765fcde15ded56 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -59,3 +59,37 @@ lemma pic_inv_d_dx (p) (k):
       p◖𝗱k ϵ 𝐈 → ⊥.
 #p #k #H0 @H0 -H0 //
 qed-.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma pic_m_sn (p):
+      p ϵ 𝐈 → 𝗺◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_L_sn (p):
+      p ϵ 𝐈 → 𝗟◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_A_sn (p):
+      p ϵ 𝐈 → 𝗔◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_S_sn (p):
+      p ϵ 𝐈 → 𝗦◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.