+lemma tr_compose_push_bi (f2) (f1):
+ (⫯(f2∘f1)) = (⫯f2)∘(⫯f1).
+#f2 #f1
+<tr_compose_unfold //
+qed.
+
+lemma tr_compose_push_next (f2) (f1):
+ ↑(f2∘f1) = (⫯f2)∘(↑f1).
+#f2 * #p1 #f1
+<tr_next_unfold <tr_compose_unfold <tr_compose_unfold <tr_next_unfold
+<tr_pap_push >nsucc_inj //
+qed.
+
+(* Note: to be removed *)