lapply (sor_comm … Hz) -Hz #Hz
lapply (sor_mono … f Hz ?) // -Hz #H
lapply (sor_inv_sle_sn … Hf) -Hf #Hf
- lapply (frees_eq_repl_back â\80¦ Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
+ lapply (frees_eq_repl_back â\80¦ Hf0 (â\86\91f) ?) /2 width=5 by eq_next/ -z #Hf0
@(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
/2 width=1 by sor_sle_dx/
]
(
∀f,L,s. 𝐈⦃f⦄ → R L (⋆s) f
) → (
- â\88\80f,i. ð\9d\90\88â¦\83fâ¦\84 â\86\92 R (â\8b\86) (#i) (â\86\91*[i]⫯f)
+ â\88\80f,i. ð\9d\90\88â¦\83fâ¦\84 â\86\92 R (â\8b\86) (#i) (⫯*[i]â\86\91f)
) → (
∀f,I,L,V.
- L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f â\86\92 R L V fâ\86\92 R (L.â\93\91{I}V) (#O) (⫯f)
+ L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f â\86\92 R L V fâ\86\92 R (L.â\93\91{I}V) (#O) (â\86\91f)
) → (
- â\88\80f,I,L. ð\9d\90\88â¦\83fâ¦\84 â\86\92 R (L.â\93¤{I}) (#O) (⫯f)
+ â\88\80f,I,L. ð\9d\90\88â¦\83fâ¦\84 â\86\92 R (L.â\93¤{I}) (#O) (â\86\91f)
) → (
∀f,I,L,i.
- L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 f â\86\92 R L (#i) f â\86\92 R (L.â\93\98{I}) (#(⫯i)) (â\86\91f)
+ L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 f â\86\92 R L (#i) f â\86\92 R (L.â\93\98{I}) (#(â\86\91i)) (⫯f)
) → (
∀f,L,l. 𝐈⦃f⦄ → R L (§l) f
) → (