+ 'UpTriangleArrow f t = (subset_ext_f1 ? ? (lift_path f) t).
+
+(* Basic constructions ******************************************************)
+
+lemma in_comp_lift_path_term (f) (t) (p):
+ p ϵ t → 🠡[f]p ϵ 🠡[f]t.
+/2 width=1 by subset_in_ext_f1_dx/
+qed.