-fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
- ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K → K2 = K →
- ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
+fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
+ ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.