(* Basic_forward lemmas *****************************************************)
-lemma lsubss_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L1|] L2.
+lemma lsubss_fwd_lsubr1: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L1|] L2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
-lemma lsubss_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\89¼[0, |L2|] L2.
+lemma lsubss_fwd_lsubr2: â\88\80h,g,L1,L2. h â\8a¢ L1 â\80¢â\8a\91[g] L2 â\86\92 L1 â\8a\91[0, |L2|] L2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.