-T).(\lambda (z: T).(eq T t (lift h d z))))) H1)))]) in (H0 (refl_equal T
-(lift h d (TSort n))))))))) (\lambda (n: nat).(\lambda (h: nat).(\lambda (d:
-nat).(\lambda (H: (eq T (THead (Flat f) u t) (lift h d (TLRef n)))).(lt_le_e
-n d (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat
-f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
-(_: T).(\lambda (z: T).(eq T t (lift h d z))))) (\lambda (H0: (lt n d)).(let
-H1 \def (eq_ind T (lift h d (TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f)
-u t) t0)) H (TLRef n) (lift_lref_lt n h d H0)) in (let H2 \def (match H1 in
-eq return (\lambda (t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef n)) \to
-(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y
-z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
-(\lambda (H2: (eq T (THead (Flat f) u t) (TLRef n))).(let H3 \def (eq_ind T
-(THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
-(THead _ _ _) \Rightarrow True])) I (TLRef n) H2) in (False_ind (ex3_2 T T
-(\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z))))
-(\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t (lift h d z))))) H3)))]) in (H2 (refl_equal T
-(TLRef n)))))) (\lambda (H0: (le d n)).(let H1 \def (eq_ind T (lift h d
-(TLRef n)) (\lambda (t0: T).(eq T (THead (Flat f) u t) t0)) H (TLRef (plus n
-h)) (lift_lref_ge n h d H0)) in (let H2 \def (match H1 in eq return (\lambda
-(t0: T).(\lambda (_: (eq ? ? t0)).((eq T t0 (TLRef (plus n h))) \to (ex3_2 T
-T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y z))))
-(\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t (lift h d z)))))))) with [refl_equal \Rightarrow
-(\lambda (H2: (eq T (THead (Flat f) u t) (TLRef (plus n h)))).(let H3 \def
-(eq_ind T (THead (Flat f) u t) (\lambda (e: T).(match e in T return (\lambda
-(_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
-| (THead _ _ _) \Rightarrow True])) I (TLRef (plus n h)) H2) in (False_ind
-(ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T (TLRef n) (THead (Flat f) y
-z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t (lift h d z))))) H3)))]) in (H2 (refl_equal T
-(TLRef (plus n h)))))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_:
-((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h d
-t0)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t0 (THead (Flat f)
-y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda (_:
-T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (t1: T).(\lambda
-(_: ((\forall (h: nat).(\forall (d: nat).((eq T (THead (Flat f) u t) (lift h
-d t1)) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T t1 (THead (Flat
-f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T u (lift h d y)))) (\lambda
-(_: T).(\lambda (z: T).(eq T t (lift h d z)))))))))).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (H1: (eq T (THead (Flat f) u t) (lift h d
-(THead k t0 t1)))).(let H2 \def (eq_ind T (lift h d (THead k t0 t1)) (\lambda
-(t2: T).(eq T (THead (Flat f) u t) t2)) H1 (THead k (lift h d t0) (lift h (s
-k d) t1)) (lift_head k t0 t1 h d)) in (let H3 \def (match H2 in eq return
-(\lambda (t2: T).(\lambda (_: (eq ? ? t2)).((eq T t2 (THead k (lift h d t0)
-(lift h (s k d) t1))) \to (ex3_2 T T (\lambda (y: T).(\lambda (z: T).(eq T
-(THead k t0 t1) (THead (Flat f) y z)))) (\lambda (y: T).(\lambda (_: T).(eq T
-u (lift h d y)))) (\lambda (_: T).(\lambda (z: T).(eq T t (lift h d z))))))))
-with [refl_equal \Rightarrow (\lambda (H3: (eq T (THead (Flat f) u t) (THead
-k (lift h d t0) (lift h (s k d) t1)))).(let H4 \def (f_equal T T (\lambda (e:
-T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t |
-(TLRef _) \Rightarrow t | (THead _ _ t2) \Rightarrow t2])) (THead (Flat f) u
-t) (THead k (lift h d t0) (lift h (s k d) t1)) H3) in ((let H5 \def (f_equal
-T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
-\Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t2 _) \Rightarrow t2]))
-(THead (Flat f) u t) (THead k (lift h d t0) (lift h (s k d) t1)) H3) in ((let
-H6 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K)
-with [(TSort _) \Rightarrow (Flat f) | (TLRef _) \Rightarrow (Flat f) |
-(THead k0 _ _) \Rightarrow k0])) (THead (Flat f) u t) (THead k (lift h d t0)
-(lift h (s k d) t1)) H3) in (eq_ind K (Flat f) (\lambda (k0: K).((eq T u
-(lift h d t0)) \to ((eq T t (lift h (s k0 d) t1)) \to (ex3_2 T T (\lambda (y:
-T).(\lambda (z: T).(eq T (THead k0 t0 t1) (THead (Flat f) y z)))) (\lambda