| 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 0 (e + 1) (L1. 𝕓{Abbr} V) (L2.𝕓{Abbr} V)
+ lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
- lsubs 0 (e + 1) (L1. 𝕓{Abst} V1) (L2.𝕓{I} V2)
+ lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2)
| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- lsubs d e L1 L2 → lsubs (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
+ lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
.
interpretation
qed.
lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
- L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
+ L1. ⓑ{I} V [0, e + 1] ≼ L2.ⓑ{I} V.
#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
qed.
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.
#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
qed.