- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
- (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
- â\88\80G,L,T1. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
- â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89¡[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_lstas h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h o G1 L1 T1) →
+ (â\88\80G1,L1,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h o G1 L1 T1) →
+ â\88\80G,L,T1. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, o] →
+ â\88\80T2. â¦\83G0, L0, T0â¦\84 >â\89\9b[h, o] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, o] →