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.