-lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) →
- ∀L1,L2. TC … (lpx_sn R) L1 L2 →
- ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V).
-#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2
-[ /2 width=1 by lpx_sn_refl/
-| /3 width=1 by TC_reflexive, lpx_sn_refl/
-| /3 width=5 by lpx_sn_pair, step/
-]
-qed-.
-
-lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) →
- ∀I,L1,L2. TC … (lpx_sn R) L1 L2 →
- ∀V1,V2. LTC … R L1 V1 V2 →
- TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2).
-#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 //
-[ /2 width=1 by TC_lpx_sn_pair_refl/
-| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/
-]
-qed-.
-