[ list_empty โ k f (๐)
| list_lcons l q โ
match l with
- [ label_node_d n โ
+ [ label_d n โ
match q with
[ list_empty โ lift_gen (A) (ฮปg,p. k g (๐ฑ(f@โจnโฉ)โp)) (fโ๐ฎโจnโฉ) q
| list_lcons _ _ โ lift_gen (A) k (fโ๐ฎโจnโฉ) q
]
- | label_edge_L โ lift_gen (A) (ฮปg,p. k g (๐โp)) (โซฏf) q
- | label_edge_A โ lift_gen (A) (ฮปg,p. k g (๐โp)) f q
- | label_edge_S โ lift_gen (A) (ฮปg,p. k g (๐ฆโp)) f q
+ | label_m โ lift_gen (A) k f q
+ | label_L โ lift_gen (A) (ฮปg,p. k g (๐โp)) (โซฏf) q
+ | label_A โ lift_gen (A) (ฮปg,p. k g (๐โp)) f q
+ | label_S โ lift_gen (A) (ฮปg,p. k g (๐ฆโp)) f q
]
].
โโจk, fโ๐ฎโจninj nโฉ, lโpโฉ = โ{A}โจk, f, ๐ฑnโlโpโฉ.
// qed.
+lemma lift_m_sn (A) (k) (p) (f):
+ โโจk, f, pโฉ = โ{A}โจk, f, ๐บโpโฉ.
+// qed.
+
lemma lift_L_sn (A) (k) (p) (f):
โโจ(ฮปg,p. k g (๐โp)), โซฏf, pโฉ = โ{A}โจk, f, ๐โpโฉ.
// qed.
โ[fโ๐ฎโจninj nโฉ](lโp) = โ[f](๐ฑnโlโp).
// qed.
+lemma lift_path_m_sn (f) (p):
+ โ[f]p = โ[f](๐บโp).
+// qed.
+
(* Basic constructions with proj_rmap ***************************************)
+lemma lift_rmap_empty (f):
+ f = โ[๐]f.
+// qed.
+
lemma lift_rmap_d_sn (f) (p) (n):
โ[p](fโ๐ฎโจninj nโฉ) = โ[๐ฑnโp]f.
#f * // qed.
+lemma lift_rmap_m_sn (f) (p):
+ โ[p]f = โ[๐บโp]f.
+// qed.
+
lemma lift_rmap_L_sn (f) (p):
โ[p](โซฏf) = โ[๐โp]f.
// qed.
lemma lift_rmap_append (p2) (p1) (f):
โ[p2]โ[p1]f = โ[p1โp2]f.
#p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f //
-[ <lift_rmap_A_sn <lift_rmap_A_sn //
+[ <lift_rmap_m_sn <lift_rmap_m_sn //
+| <lift_rmap_A_sn <lift_rmap_A_sn //
| <lift_rmap_S_sn <lift_rmap_S_sn //
]
qed.
+(* Advanced constructions with proj_rmap and path_rcons *********************)
+
+lemma lift_rmap_d_dx (f) (p) (n):
+ (โ[p]f)โ๐ฎโจninj nโฉ = โ[pโ๐ฑn]f.
+// qed.
+
+lemma lift_rmap_m_dx (f) (p):
+ โ[p]f = โ[pโ๐บ]f.
+// qed.
+
+lemma lift_rmap_L_dx (f) (p):
+ (โซฏโ[p]f) = โ[pโ๐]f.
+// qed.
+
+lemma lift_rmap_A_dx (f) (p):
+ โ[p]f = โ[pโ๐]f.
+// qed.
+
+lemma lift_rmap_S_dx (f) (p):
+ โ[p]f = โ[pโ๐ฆ]f.
+// qed.
+
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate โฆ):
Q (๐) โ
(โn. Q (๐) โ Q (๐ฑnโ๐)) โ
(โn,l,p. Q (lโp) โ Q (๐ฑnโlโp)) โ
+ (โp. Q p โ Q (๐บโp)) โ
(โp. Q p โ Q (๐โp)) โ
(โp. Q p โ Q (๐โp)) โ
(โp. Q p โ Q (๐ฆโp)) โ
โp. Q p.
-#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #p
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
elim p -p [| * [ #n * ] ]
/2 width=1 by/
qed-.