(* *)
(**************************************************************************)
-include "basic_2/substitution/lleq_lleq.ma".
+include "basic_2/multiple/lleq_lleq.ma".
include "basic_2/reduction/lpx_lleq.ma".
include "basic_2/computation/lsx.ma".
(* Advanced properties ******************************************************)
lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⬊*[h, g, T, d] L1 →
- â\88\80L2. L1 â\8b\95[T, d] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+ â\88\80L2. L1 â\89¡[T, d] L2 → G ⊢ ⬊*[h, g, T, d] L2.
#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1
#L1 #_ #IHL1 #L2 #HL12 @lsx_intro
#K2 #HLK2 #HnLK2 elim (lleq_lpx_trans … HLK2 … HL12) -HLK2
qed-.
lemma lsx_leq_conf: ∀h,g,G,L1,T,d. G ⊢ ⬊*[h, g, T, d] L1 →
- â\88\80L2. L1 â\89\83[d, ∞] L2 → G ⊢ ⬊*[h, g, T, d] L2.
+ â\88\80L2. L1 ⩬[d, ∞] L2 → G ⊢ ⬊*[h, g, T, d] L2.
#h #g #G #L1 #T #d #H @(lsx_ind … H) -L1
#L1 #_ #IHL1 #L2 #HL12 @lsx_intro
#L3 #HL23 #HnL23 elim (leq_lpx_trans_lleq … HL12 … HL23) -HL12 -HL23