lemma lift_d_empty_dx (n) (p) (f):
(āp)āš±āØ(ā[pāš±āØnā©]f)@āØnā©ā© = ā[f](pāš±āØnā©).
-#n #p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| <list_cons_shift <list_cons_comm <list_cons_comm //
-| <lift_d_lcons_sn <lift_d_lcons_sn //
-| <lift_L_sn <lift_L_sn <lift_lcons <IH //
-| <lift_A_sn <lift_A_sn <lift_lcons <IH //
-| <lift_S_sn <lift_S_sn <lift_lcons <IH //
+#n #p @(path_ind_lift ā¦ p) -p // [ #m #l #p |*: #p ] #IH #f
+[ <lift_rmap_d_lcons_sn <lift_path_d_lcons_sn //
+| <lift_rmap_L_sn <lift_path_L_sn <IH //
+| <lift_rmap_A_sn <lift_path_A_sn <IH //
+| <lift_rmap_S_sn <lift_path_S_sn <IH //
]
qed.
lemma lift_L_dx (p) (f):
(āp)āš = ā[f](pāš).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
qed.
lemma lift_A_dx (p) (f):
(āp)āš = ā[f](pāš).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
qed.
lemma lift_S_dx (p) (f):
(āp)āš¦ = ā[f](pāš¦).
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| <lift_d_lcons_sn //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift ā¦ p) -p // #m #l #p #IH #f
+<lift_path_d_lcons_sn //
qed.
lemma structure_lift (p) (f):
āp = āā[f]p.
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| //
-| <lift_L_sn <lift_lcons //
-| <lift_A_sn <lift_lcons //
-| <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift ā¦ p) -p // #p #IH #f
+<lift_path_L_sn //
qed.
lemma lift_structure (p) (f):
āp = ā[f]āp.
-#p elim p -p
-[| * [ #m * [| #l ]] [|*: #p ] #IH ] #f
-[ //
-| //
-| //
-| <structure_L_sn <lift_L_sn <lift_lcons //
-| <structure_A_sn <lift_A_sn <lift_lcons //
-| <structure_S_sn <lift_S_sn <lift_lcons //
-]
+#p @(path_ind_lift ā¦ p) -p //
qed.