-lemma fle_sort: ∀L1,L2,s1,s2. ⦃L1, ⋆s1⦄ ⊆ ⦃L2, ⋆s2⦄.
-/3 width=5 by frees_sort, sle_refl, ex3_2_intro/ qed.
-
-lemma fle_gref: ∀L1,L2,l1,l2. ⦃L1, §l1⦄ ⊆ ⦃L2, §l2⦄.
-/3 width=5 by frees_gref, sle_refl, ex3_2_intro/ qed.
-
-lemma fle_bind: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ⊆ ⦃L2, V2⦄ →
- ∀I1,I2,T1,T2. ⦃L1.ⓑ{I1}V1, T1⦄ ⊆ ⦃L2.ⓑ{I2}V2, T2⦄ →
- ∀p. ⦃L1, ⓑ{p,I1}V1.T1⦄ ⊆ ⦃L2, ⓑ{p,I2}V2.T2⦄.
-#L1 #L2 #V1 #V2 * #f1 #g1 #HV1 #HV2 #Hfg1 #I1 #I2 #T1 #T2 * #f2 #g2 #Hf2 #Hg2 #Hfg2 #p
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
-/4 width=12 by frees_bind, monotonic_sle_sor, sle_tl, ex3_2_intro/
+lemma fle_sort: ∀L,s1,s2. ⦃L, ⋆s1⦄ ⊆ ⦃L, ⋆s2⦄.
+#L elim (lveq_refl L)
+/3 width=8 by frees_sort, sle_refl, ex4_4_intro/