| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2
| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2
| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
qed.
lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
qed.
lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
qed.
lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d →
qed.
lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≼ L2. 𝕓{I2} V2.
+ ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 [d, e] ≼ L2. ⓑ{I2} V2.