\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t
(TSort m)) \to ((nf2 c t) \to (or (ex2 nat (\lambda (n: nat).(eq T t (TSort
n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws:
\forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t
(TSort m)) \to ((nf2 c t) \to (or (ex2 nat (\lambda (n: nat).(eq T t (TSort
n))) (\lambda (n: nat).(eq nat m (next g n)))) (ex3_2 TList nat (\lambda (ws: