-n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3 (CHead d (Bind Abbr) u) H0)
-in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_: C).(drop n O c0 e0)))
-(\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n) e0 e1))) (\lambda (_:
-C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abbr) u)))) (ty3 g c0 (lift h d0
-(TLRef n)) (lift h d0 (lift (S n) O t))) (\lambda (x0: C).(\lambda (x1:
-C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop h (minus d0 n) x0
-x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abbr) u))).(let H9 \def (eq_ind
-nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S
-n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0 h (minus d0
-(S n)) H9 Abbr d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0 (CHead c1
-(Bind Abbr) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h (minus d0
-(S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O t)))
-(\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr) (lift h (minus
-d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x d)).(eq_ind_r T
-(TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t))))
-(eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3 g c0 (TLRef
-n) (lift h n0 (lift (S n) O t)))) (eq_ind_r T (lift (S n) O (lift h (minus d0
-(S n)) t)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda
-(_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S n)) t))))
-(ty3_abbr g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0 (CHead x
-(Bind Abbr) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus d0 (S n))
-t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
-(le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
-n) O t)) (lift_d t h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
-(le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
-H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
-h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O t)))) (eq_ind nat
-(S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
-t)))) (eq_ind_r T (lift (plus h (S n)) O t) (\lambda (t0: T).(ty3 g c0 (TLRef
-(plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
-(TLRef (plus n h)) (lift n0 O t))) (ty3_abbr g (plus n h) c0 d u
-(drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abbr) u) H0 H4) t H1) (plus
-h (S n)) (plus_sym h (S n))) (lift h d0 (lift (S n) O t)) (lift_free t (S n)
-h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
-n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
-(plus n (S O)) (plus_sym n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
-d0 H4)))))))))))))))) (\lambda (n: nat).(\lambda (c: C).(\lambda (d:
-C).(\lambda (u: T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda
-(t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c0: C).(\forall
-(d0: nat).(\forall (h: nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u)
-(lift h d0 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h:
-nat).(\lambda (H3: (drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0
-(TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda (H4: (lt n d0)).(let H5
-\def (drop_getl_trans_le n d0 (le_S_n n d0 (le_S (S n) d0 H4)) c0 c h H3
-(CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda (e0: C).(\lambda (_:
-C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d0 n)
-e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1 (CHead d (Bind Abst)
-u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda
-(x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop
-h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) u))).(let
-H9 \def (eq_ind nat (minus d0 n) (\lambda (n0: nat).(drop h n0 x0 x1)) H7 (S
-(minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let H10 \def (drop_clear_S x1 x0
-h (minus d0 (S n)) H9 Abst d u H8) in (ex2_ind C (\lambda (c1: C).(clear x0
-(CHead c1 (Bind Abst) (lift h (minus d0 (S n)) u)))) (\lambda (c1: C).(drop h
-(minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift (S
-n) O u))) (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift
-h (minus d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x
-d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S
-n) O u)))) (eq_ind nat (plus (S n) (minus d0 (S n))) (\lambda (n0: nat).(ty3
-g c0 (TLRef n) (lift h n0 (lift (S n) O u)))) (eq_ind_r T (lift (S n) O (lift
-h (minus d0 (S n)) u)) (\lambda (t0: T).(ty3 g c0 (TLRef n) t0)) (eq_ind nat
-d0 (\lambda (_: nat).(ty3 g c0 (TLRef n) (lift (S n) O (lift h (minus d0 (S
-n)) u)))) (ty3_abst g n c0 x (lift h (minus d0 (S n)) u) (getl_intro n c0
-(CHead x (Bind Abst) (lift h (minus d0 (S n)) u)) x0 H6 H11) (lift h (minus
-d0 (S n)) t) (H2 x (minus d0 (S n)) h H12)) (plus (S n) (minus d0 (S n)))
-(le_plus_minus (S n) d0 H4)) (lift h (plus (S n) (minus d0 (S n))) (lift (S
-n) O u)) (lift_d u h (S n) (minus d0 (S n)) O (le_O_n (minus d0 (S n))))) d0
-(le_plus_minus_r (S n) d0 H4)) (lift h d0 (TLRef n)) (lift_lref_lt n h d0
-H4))))) H10)))))))) H5))) (\lambda (H4: (le d0 n)).(eq_ind_r T (TLRef (plus n
-h)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d0 (lift (S n) O u)))) (eq_ind nat
-(S n) (\lambda (_: nat).(ty3 g c0 (TLRef (plus n h)) (lift h d0 (lift (S n) O
-u)))) (eq_ind_r T (lift (plus h (S n)) O u) (\lambda (t0: T).(ty3 g c0 (TLRef
-(plus n h)) t0)) (eq_ind_r nat (plus (S n) h) (\lambda (n0: nat).(ty3 g c0
-(TLRef (plus n h)) (lift n0 O u))) (ty3_abst g (plus n h) c0 d u
-(drop_getl_trans_ge n c0 c d0 h H3 (CHead d (Bind Abst) u) H0 H4) t H1) (plus
-h (S n)) (plus_sym h (S n))) (lift h d0 (lift (S n) O u)) (lift_free u (S n)
-h O d0 (le_S d0 n H4) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
-n) (\lambda (n0: nat).(eq nat (S n) n0)) (refl_equal nat (plus (S O) n))
-(plus n (S O)) (plus_sym n (S O)))) (lift h d0 (TLRef n)) (lift_lref_ge n h
-d0 H4)))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (t:
-T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
-nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d
-t)))))))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3
-g (CHead c (Bind b) u) t0 t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d:
-nat).(\forall (h: nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0
-(lift h d t0) (lift h d t3)))))))).(\lambda (c0: C).(\lambda (d:
-nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead
-(Bind b) (lift h d u) (lift h (s (Bind b) d) t0)) (\lambda (t4: T).(ty3 g c0
-t4 (lift h d (THead (Bind b) u t3)))) (eq_ind_r T (THead (Bind b) (lift h d
-u) (lift h (s (Bind b) d) t3)) (\lambda (t4: T).(ty3 g c0 (THead (Bind b)
-(lift h d u) (lift h (s (Bind b) d) t0)) t4)) (ty3_bind g c0 (lift h d u)
-(lift h d t) (H1 c0 d h H4) b (lift h (S d) t0) (lift h (S d) t3) (H3 (CHead
-c0 (Bind b) (lift h d u)) (S d) h (drop_skip_bind h d c0 c H4 b u))) (lift h
-d (THead (Bind b) u t3)) (lift_head (Bind b) u t3 h d)) (lift h d (THead
-(Bind b) u t0)) (lift_head (Bind b) u t0 h d)))))))))))))))) (\lambda (c:
-C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1:
-((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
-(ty3 g c0 (lift h d w) (lift h d u)))))))).(\lambda (v: T).(\lambda (t:
-T).(\lambda (_: (ty3 g c v (THead (Bind Abst) u t))).(\lambda (H3: ((\forall
-(c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0
-(lift h d v) (lift h d (THead (Bind Abst) u t))))))))).(\lambda (c0:
-C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: (drop h d c0
-c)).(eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v))
-(\lambda (t0: T).(ty3 g c0 t0 (lift h d (THead (Flat Appl) w (THead (Bind
-Abst) u t))))) (eq_ind_r T (THead (Flat Appl) (lift h d w) (lift h (s (Flat
-Appl) d) (THead (Bind Abst) u t))) (\lambda (t0: T).(ty3 g c0 (THead (Flat
-Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) t0)) (eq_ind_r T (THead
-(Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s (Bind Abst) (s (Flat
-Appl) d)) t)) (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w)
-(lift h (s (Flat Appl) d) v)) (THead (Flat Appl) (lift h d w) t0))) (ty3_appl
-g c0 (lift h d w) (lift h d u) (H1 c0 d h H4) (lift h d v) (lift h (S d) t)
-(eq_ind T (lift h d (THead (Bind Abst) u t)) (\lambda (t0: T).(ty3 g c0 (lift
-h d v) t0)) (H3 c0 d h H4) (THead (Bind Abst) (lift h d u) (lift h (S d) t))
-(lift_bind Abst u t h d))) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t))
-(lift_head (Bind Abst) u t h (s (Flat Appl) d))) (lift h d (THead (Flat Appl)
-w (THead (Bind Abst) u t))) (lift_head (Flat Appl) w (THead (Bind Abst) u t)
-h d)) (lift h d (THead (Flat Appl) w v)) (lift_head (Flat Appl) w v h
-d))))))))))))))) (\lambda (c: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda
-(_: (ty3 g c t0 t3)).(\lambda (H1: ((\forall (c0: C).(\forall (d:
-nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t0) (lift h d
-t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g c t3 t4)).(\lambda (H3:
+n d0 (le_S_n n d0 (le_S_n (S n) (S d0) (le_S (S (S n)) (S d0) (le_n_S (S n)
+d0 H4)))) c0 c h H3 (CHead d (Bind Abbr) u) H0) in (ex3_2_ind C C (\lambda
+(e0: C).(\lambda (_: C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1:
+C).(drop h (minus d0 n) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1
+(CHead d (Bind Abbr) u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift
+(S n) O t))) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0
+x0)).(\lambda (H7: (drop h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1
+(CHead d (Bind Abbr) u))).(let H9 \def (eq_ind nat (minus d0 n) (\lambda (n0:
+nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let
+H10 \def (drop_clear_S x1 x0 h (minus d0 (S n)) H9 Abbr d u H8) in (ex2_ind C
+(\lambda (c1: C).(clear x0 (CHead c1 (Bind Abbr) (lift h (minus d0 (S n))
+u)))) (\lambda (c1: C).(drop h (minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0
+(TLRef n)) (lift h d0 (lift (S n) O t))) (\lambda (x: C).(\lambda (H11:
+(clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S n)) u)))).(\lambda (H12:
+(drop h (minus d0 (S n)) x d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g
+c0 t0 (lift h d0 (lift (S n) O t)))) (eq_ind nat (plus (S n) (minus d0 (S
+n))) (\lambda (n0: nat).(ty3 g c0 (TLRef n) (lift h n0 (lift (S n) O t))))
+(eq_ind_r T (lift (S n) O (lift h (minus d0 (S n)) t)) (\lambda (t0: T).(ty3
+g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda (_: nat).(ty3 g c0 (TLRef n)
+(lift (S n) O (lift h (minus d0 (S n)) t)))) (ty3_abbr g n c0 x (lift h
+(minus d0 (S n)) u) (getl_intro n c0 (CHead x (Bind Abbr) (lift h (minus d0
+(S n)) u)) x0 H6 H11) (lift h (minus d0 (S n)) t) (H2 x (minus d0 (S n)) h
+H12)) (plus (S n) (minus d0 (S n))) (le_plus_minus (S n) d0 H4)) (lift h
+(plus (S n) (minus d0 (S n))) (lift (S n) O t)) (lift_d t h (S n) (minus d0
+(S n)) O (le_O_n (minus d0 (S n))))) d0 (le_plus_minus_r (S n) d0 H4)) (lift
+h d0 (TLRef n)) (lift_lref_lt n h d0 H4))))) H10)))))))) H5))) (\lambda (H4:
+(le d0 n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(ty3 g c0 t0 (lift
+h d0 (lift (S n) O t)))) (eq_ind nat (S n) (\lambda (_: nat).(ty3 g c0 (TLRef
+(plus n h)) (lift h d0 (lift (S n) O t)))) (eq_ind_r T (lift (plus h (S n)) O
+t) (\lambda (t0: T).(ty3 g c0 (TLRef (plus n h)) t0)) (eq_ind_r nat (plus (S
+n) h) (\lambda (n0: nat).(ty3 g c0 (TLRef (plus n h)) (lift n0 O t)))
+(ty3_abbr g (plus n h) c0 d u (drop_getl_trans_ge n c0 c d0 h H3 (CHead d
+(Bind Abbr) u) H0 H4) t H1) (plus h (S n)) (plus_sym h (S n))) (lift h d0
+(lift (S n) O t)) (lift_free t (S n) h O d0 (le_S_n d0 (S n) (le_S (S d0) (S
+n) (le_n_S d0 n H4))) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
+n) (\lambda (n0: nat).(eq nat (S n) n0)) (le_antisym (S n) (plus (S O) n)
+(le_n (plus (S O) n)) (le_n (S n))) (plus n (S O)) (plus_sym n (S O)))) (lift
+h d0 (TLRef n)) (lift_lref_ge n h d0 H4)))))))))))))))) (\lambda (n:
+nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c
+(CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u
+t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0: nat).(\forall (h:
+nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h d0
+t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda (H3:
+(drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0
+(lift (S n) O u))) (\lambda (H4: (lt n d0)).(let H5 \def (drop_getl_trans_le
+n d0 (le_S_n n d0 (le_S_n (S n) (S d0) (le_S (S (S n)) (S d0) (le_n_S (S n)
+d0 H4)))) c0 c h H3 (CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda
+(e0: C).(\lambda (_: C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1:
+C).(drop h (minus d0 n) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1
+(CHead d (Bind Abst) u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift
+(S n) O u))) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0
+x0)).(\lambda (H7: (drop h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1
+(CHead d (Bind Abst) u))).(let H9 \def (eq_ind nat (minus d0 n) (\lambda (n0:
+nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let
+H10 \def (drop_clear_S x1 x0 h (minus d0 (S n)) H9 Abst d u H8) in (ex2_ind C
+(\lambda (c1: C).(clear x0 (CHead c1 (Bind Abst) (lift h (minus d0 (S n))
+u)))) (\lambda (c1: C).(drop h (minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0
+(TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda (x: C).(\lambda (H11:
+(clear x0 (CHead x (Bind Abst) (lift h (minus d0 (S n)) u)))).(\lambda (H12:
+(drop h (minus d0 (S n)) x d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g
+c0 t0 (lift h d0 (lift (S n) O u)))) (eq_ind nat (plus (S n) (minus d0 (S
+n))) (\lambda (n0: nat).(ty3 g c0 (TLRef n) (lift h n0 (lift (S n) O u))))
+(eq_ind_r T (lift (S n) O (lift h (minus d0 (S n)) u)) (\lambda (t0: T).(ty3
+g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda (_: nat).(ty3 g c0 (TLRef n)
+(lift (S n) O (lift h (minus d0 (S n)) u)))) (ty3_abst g n c0 x (lift h
+(minus d0 (S n)) u) (getl_intro n c0 (CHead x (Bind Abst) (lift h (minus d0
+(S n)) u)) x0 H6 H11) (lift h (minus d0 (S n)) t) (H2 x (minus d0 (S n)) h
+H12)) (plus (S n) (minus d0 (S n))) (le_plus_minus (S n) d0 H4)) (lift h
+(plus (S n) (minus d0 (S n))) (lift (S n) O u)) (lift_d u h (S n) (minus d0
+(S n)) O (le_O_n (minus d0 (S n))))) d0 (le_plus_minus_r (S n) d0 H4)) (lift
+h d0 (TLRef n)) (lift_lref_lt n h d0 H4))))) H10)))))))) H5))) (\lambda (H4:
+(le d0 n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(ty3 g c0 t0 (lift
+h d0 (lift (S n) O u)))) (eq_ind nat (S n) (\lambda (_: nat).(ty3 g c0 (TLRef
+(plus n h)) (lift h d0 (lift (S n) O u)))) (eq_ind_r T (lift (plus h (S n)) O
+u) (\lambda (t0: T).(ty3 g c0 (TLRef (plus n h)) t0)) (eq_ind_r nat (plus (S
+n) h) (\lambda (n0: nat).(ty3 g c0 (TLRef (plus n h)) (lift n0 O u)))
+(ty3_abst g (plus n h) c0 d u (drop_getl_trans_ge n c0 c d0 h H3 (CHead d
+(Bind Abst) u) H0 H4) t H1) (plus h (S n)) (plus_sym h (S n))) (lift h d0
+(lift (S n) O u)) (lift_free u (S n) h O d0 (le_S_n d0 (S n) (le_S (S d0) (S
+n) (le_n_S d0 n H4))) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
+n) (\lambda (n0: nat).(eq nat (S n) n0)) (le_antisym (S n) (plus (S O) n)
+(le_n (plus (S O) n)) (le_n (S n))) (plus n (S O)) (plus_sym n (S O)))) (lift
+h d0 (TLRef n)) (lift_lref_ge n h d0 H4)))))))))))))))) (\lambda (c:
+C).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c u t)).(\lambda (H1: