(* Note: inner numeric labels are not liftable, so they are removed *)
rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p ā
match p with
-[ list_empty ā k š f
+[ list_empty ā k (š) f
| list_lcons l q ā
match l with
[ label_node_d n ā
(* Basic constructions ******************************************************)
lemma lift_empty (A) (k) (f):
- k š f = ā{A}āØk, š, fā©.
+ k (š) f = ā{A}āØk, š, fā©.
// qed.
lemma lift_d_empty_sn (A) (k) (n) (f):
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate ā¦):
- Q š ā
- (ān. Q š ā Q (š±āØnā©āš)) ā
+ 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)) ā