\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (i: nat).((ty3 g c
(TLRef i) u1) \to ((nf2 c (TLRef i)) \to (\forall (u2: T).((nf2 c u2) \to
((pc3 c u1 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))))
\forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (i: nat).((ty3 g c
(TLRef i) u1) \to ((nf2 c (TLRef i)) \to (\forall (u2: T).((nf2 c u2) \to
((pc3 c u1 u2) \to (ex T (\lambda (u: T).(eq T u2 (lift (S i) O u))))))))))))