(* INNER CONDITION FOR PATH *************************************************)
definition pic: predicate path ā
- Ī»p. āq,n. qāš±n = p ā ā„
+ Ī»p. āq,k. qāš±k = p ā ā„
.
interpretation
(* Basic constructions ******************************************************)
-lemma pic_empty: š Ļµ š.
-#q #n #H0
-elim (eq_inv_list_empty_rcons ??? (sym_eq ā¦ H0))
+lemma pic_empty:
+ (š) Ļµ š.
+#q #k #H0 destruct
qed.
-lemma pic_m_dx (p): pāšŗ Ļµ š.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_m_dx (p):
+ pāšŗ Ļµ š.
+#p #q #k #H0 destruct
qed.
-lemma pic_L_dx (p): pāš Ļµ š.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_L_dx (p):
+ pāš Ļµ š.
+#p #q #k #H0 destruct
qed.
-lemma pic_A_dx (p): pāš Ļµ š.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_A_dx (p):
+ pāš Ļµ š.
+#p #q #k #H0 destruct
qed.
-lemma pic_S_dx (p): pāš¦ Ļµ š.
-#p #q #n #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #_ #H0 destruct
+lemma pic_S_dx (p):
+ pāš¦ Ļµ š.
+#p #q #k #H0 destruct
qed.
(* Basic inversions ********************************************************)
-lemma pic_inv_d_dx (p) (n):
- pāš±n Ļµ š ā ā„.
-#p #n #H0 @H0 -H0 //
+lemma pic_inv_d_dx (p) (k):
+ pāš±k Ļµ š ā ā„.
+#p #k #H0 @H0 -H0 //
qed-.