-(* Constructions with list_append *******************************************)
-
-lemma unwind2_rmap_append (f) (p1) (p2):
- ▶[▶[f]p2]p1 = ▶[f](p1●p2).
-#f #p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 //
-[ <unwind2_rmap_m_sn <unwind2_rmap_m_sn //
-| <unwind2_rmap_L_sn <unwind2_rmap_L_sn //
-| <unwind2_rmap_A_sn <unwind2_rmap_A_sn //
-| <unwind2_rmap_S_sn <unwind2_rmap_S_sn //
-]
+(* Constructions with path_append *******************************************)
+
+lemma unwind2_rmap_append (f) (p) (q):
+ ▶[▶[f]p]q = ▶[f](p●q).
+#f #p #q elim q -q // #l #q #IH
+<unwind2_rmap_rcons <unwind2_rmap_rcons //