- elim (cofrees_inv_bind ā¦ HX1) -HX1 #HV1 #HU1
- @cofrees_bind [ /3 width=7 by cofrees_flat/ ]
- @(cofrees_lsuby_conf (L2.āV2)) /3 width=7 by lpx_pair, lsuby_succ/
- |
-
-
-*)
+ elim (frees_inv_bind ā¦ Hi) -Hi #Hi
+ [ elim (frees_inv_flat ā¦ Hi) -Hi
+ /4 width=7 by frees_flat_dx, frees_flat_sn, frees_bind_sn/
+ | lapply (leq_frees_trans ā¦ Hi (L2.āV2) ?) /2 width=1 by leq_succ/ -Hi #HU2
+ lapply (frees_weak ā¦ HU2 0 ?) -HU2
+ /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
+ ]
+ | #b #W2 #W0 #V1 #V2 #U1 #U2 #HW12 #HW20 #HV12 #HU12 #H1 #H2 #H3 destruct
+ elim (frees_inv_bind_O ā¦ Hi) -Hi #Hi
+ [ /4 width=7 by frees_flat_dx, frees_bind_sn/
+ | elim (frees_inv_flat ā¦ Hi) -Hi
+ [ #HW0 lapply (frees_inv_lift_ge ā¦ HW0 L2 (ā») ā¦ HW20 ?) -W0
+ /3 width=7 by frees_flat_sn, ldrop_drop/
+ | /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
+ ]
+ ]
+ ]
+]
+qed-.
+
+lemma cpx_frees_trans: āh,g,G. frees_trans (cpx h g G).
+/2 width=8 by lpx_cpx_frees_trans/ qed-.
+
+lemma lpx_frees_trans: āh,g,G,L1,L2. ā¦G, L1ā¦ ā¢ ā”[h, g] L2 ā
+ āU,i. L2 ā¢ i Ļµ š
*[0]ā¦Uā¦ ā L1 ā¢ i Ļµ š
*[0]ā¦Uā¦.
+/2 width=8 by lpx_cpx_frees_trans/ qed-.