- ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩.
-#f #p #n #m
-<lift_rmap_d_dx <tr_compose_pap <tr_uni_pap //
-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 #IH7 #p
-elim p -p [| * [ #n * ] ]
-/2 width=1 by/
-qed-.