-fact ssta_cpcs_lpr_aux: ∀h,g,L0,T0.
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) →
- (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) →
- ∀L1,T1,T2. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T2⦄ →
- ⦃h, L1⦄ ⊢ T1 ¡[h, g] → ⦃h, L1⦄ ⊢ T2 ¡[h, g] →
- ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ →
- ∀U2,l2. ⦃h, L1⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄ →
- L1 ⊢ T1 ⬌* T2 → ∀L2. L1 ⊢ ➡ L2 →
- l1 = l2 ∧ L2 ⊢ U1 ⬌* U2.
-#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12
+fact ssta_cpcs_lpr_aux: ∀h,g,G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) →
+ ∀G,L1,T1,T2. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T2⦄ →
+ ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ⦃G, L1⦄ ⊢ T2 ¡[h, g] →
+ ∀U1,l1. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ →
+ ∀U2,l2. ⦃G, L1⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄ →
+ ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ l1 = l2 ∧ ⦃G, L2⦄ ⊢ U1 ⬌* U2.
+#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12