-(* Basic-1: was: subst1_subst1_back *)
-lemma ltps_tps_conf: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\89« U2 →
- â\88\80L1,d1,e1. L0 [d1, e1] â\89« L1 →
- â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\89« T &
- L1 â\8a¢ U2 [d1, e1] â\89« T.
-#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2
-[ /2/
+(* Basic_1: was: subst1_subst1_back *)
+lemma ltps_tps_conf: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\96¶ U2 →
+ â\88\80L1,d1,e1. L0 [d1, e1] â\96¶ L1 →
+ â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\96¶ T &
+ L1 â\8a¢ U2 [d1, e1] â\96¶ T.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ /2 width=3/