-lemma lsxa_intro_lpx: ∀h,g,G,L1,T,d.
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\8b\95[T, d] L2 â\86\92 â\8a¥) â\86\92 G â\8a¢ â¬\8aâ¬\8a*[h, g, T, d] L2) →
- G ⊢ ⬊⬊*[h, g, T, d] L1.
-#h #g #G #L1 #T #d #IH @lsxa_intro_aux
+lemma lsxa_intro_lpx: ∀h,g,G,L1,T,l.
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\89¡[T, l] L2 â\86\92 â\8a¥) â\86\92 G â\8a¢ â¬\8aâ¬\8a*[h, g, T, l] L2) →
+ G ⊢ ⬊⬊*[h, g, T, l] L1.
+#h #g #G #L1 #T #l #IH @lsxa_intro_aux