/5 width=1 by lifts_sort, lifts_lref, lifts_bind, lifts_flat/ qed.
/5 width=1 by lifts_sort, lifts_lref, lifts_bind, lifts_flat/ qed.
/6 width=3 by cpm_eps, cpm_appl, cpm_bind, cpm_delta, ApplDelta_lifts/ qed.
/6 width=3 by cpm_eps, cpm_appl, cpm_bind, cpm_delta, ApplDelta_lifts/ qed.
/4 width=3 by cpm_zeta, ApplDelta_lifts, lifts_sort, lifts_flat/ qed.
/4 width=3 by cpm_zeta, ApplDelta_lifts, lifts_sort, lifts_flat/ qed.
-lemma fqup_ApplOmega_41 (G) (L) (s0) (s): â¦\83G,L,ApplOmega4 s0 sâ¦\84 â¬\82+ â¦\83G,L,ApplOmega1 s0 sâ¦\84.
+lemma fqup_ApplOmega_41 (G) (L) (s0) (s): â\9dªG,L,ApplOmega4 s0 sâ\9d« â¬\82+ â\9dªG,L,ApplOmega1 s0 sâ\9d«.
-theorem fpbg_refl (h) (G) (L) (s0) (s): â¦\83G,L,ApplOmega1 s0 sâ¦\84 >[h] â¦\83G,L,ApplOmega1 s0 sâ¦\84.
+theorem fpbg_refl (h) (G) (L) (s0) (s): â\9dªG,L,ApplOmega1 s0 sâ\9d« >[h] â\9dªG,L,ApplOmega1 s0 sâ\9d«.