- λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2.
-
-(* Basic properties ***********************************************************)
-
-lemma lfeq_atom: ∀I. ⋆ ≡[⓪{I}] ⋆.
-/2 width=1 by lfxs_atom/ qed.
-
-lemma lfeq_sort: ∀I,L1,L2,V1,V2,s.
- L1 ≡[⋆s] L2 → L1.ⓑ{I}V1 ≡[⋆s] L2.ⓑ{I}V2.
-/2 width=1 by lfxs_sort/ qed.
-
-lemma lfeq_zero: ∀I,L1,L2,V.
- L1 ≡[V] L2 → L1.ⓑ{I}V ≡[#0] L2.ⓑ{I}V.
-/2 width=1 by lfxs_zero/ qed.
-
-lemma lfeq_lref: ∀I,L1,L2,V1,V2,i.
- L1 ≡[#i] L2 → L1.ⓑ{I}V1 ≡[#⫯i] L2.ⓑ{I}V2.
-/2 width=1 by lfxs_lref/ qed.
-
-lemma lfeq_gref: ∀I,L1,L2,V1,V2,l.
- L1 ≡[§l] L2 → L1.ⓑ{I}V1 ≡[§l] L2.ⓑ{I}V2.
-/2 width=1 by lfxs_gref/ qed.