#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
>(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶* L2 →
∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →
#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
>(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶* L2 →
∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →