include "delayed_updating/unwind/unwind2_path_lift.ma".
include "delayed_updating/unwind/unwind2_prototerm.ma".
include "delayed_updating/unwind/unwind2_path_lift.ma".
include "delayed_updating/unwind/unwind2_prototerm.ma".
▼[f2]↑[f1]t ⇔ ▼[f2∘f1]t.
#f1 #f2 #t @subset_eq_trans
[| @subset_inclusion_ext_f1_compose ]
@subset_equivalence_ext_f1_exteq #p
▼[f2]↑[f1]t ⇔ ▼[f2∘f1]t.
#f1 #f2 #t @subset_eq_trans
[| @subset_inclusion_ext_f1_compose ]
@subset_equivalence_ext_f1_exteq #p