(* Constructions with tr_after **********************************************)
lemma lift_path_after (g) (f) (p):
- ā[g]ā[f]p = ā[gāf]p.
+ š ”[g]š ”[f]p = š ”[gāf]p.
#g #f #p elim p -p //
#l #p #IH
<lift_path_rcons <lift_path_rcons <IH -IH //