lemma scpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1.
#h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by scpds_div/
lemma scpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 →
⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1.
#h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by scpds_div/