-(\forall (P: Prop).P))))) (\lambda (n: nat).(\lambda (u: T).(\lambda (d:
-nat).(\lambda (H: (eq T (THead (Bind b) u (lift (S O) d (TSort n))) (TSort
-n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead (Bind b) u (lift (S O)
-d (TSort n))) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop)
-with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead _ _
-_) \Rightarrow True])) I (TSort n) H) in (False_ind P H0))))))) (\lambda (n:
-nat).(\lambda (u: T).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind b) u
-(lift (S O) d (TLRef n))) (TLRef n))).(\lambda (P: Prop).(let H0 \def (eq_ind
-T (THead (Bind b) u (lift (S O) d (TLRef n))) (\lambda (ee: T).(match ee in T
-return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H) in
-(False_ind P H0))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (_: ((\forall
-(u: T).(\forall (d: nat).((eq T (THead (Bind b) u (lift (S O) d t)) t) \to
-(\forall (P: Prop).P)))))).(\lambda (t0: T).(\lambda (H0: ((\forall (u:
-T).(\forall (d: nat).((eq T (THead (Bind b) u (lift (S O) d t0)) t0) \to
-(\forall (P: Prop).P)))))).(\lambda (u: T).(\lambda (d: nat).(\lambda (H1:
-(eq T (THead (Bind b) u (lift (S O) d (THead k t t0))) (THead k t
-t0))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e: T).(match e
-in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow (Bind b) | (TLRef
-_) \Rightarrow (Bind b) | (THead k0 _ _) \Rightarrow k0])) (THead (Bind b) u
-(lift (S O) d (THead k t t0))) (THead k t t0) H1) in ((let H3 \def (f_equal T
-T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
-\Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t1 _) \Rightarrow t1]))
-(THead (Bind b) u (lift (S O) d (THead k t t0))) (THead k t t0) H1) in ((let
-H4 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
-with [(TSort _) \Rightarrow (THead k ((let rec lref_map (f: ((nat \to nat)))
-(d0: nat) (t1: T) on t1: T \def (match t1 with [(TSort n) \Rightarrow (TSort
-n) | (TLRef i) \Rightarrow (TLRef (match (blt i d0) with [true \Rightarrow i
-| false \Rightarrow (f i)])) | (THead k0 u0 t2) \Rightarrow (THead k0
-(lref_map f d0 u0) (lref_map f (s k0 d0) t2))]) in lref_map) (\lambda (x0:
-nat).(plus x0 (S O))) d t) ((let rec lref_map (f: ((nat \to nat))) (d0: nat)
-(t1: T) on t1: T \def (match t1 with [(TSort n) \Rightarrow (TSort n) |
-(TLRef i) \Rightarrow (TLRef (match (blt i d0) with [true \Rightarrow i |
-false \Rightarrow (f i)])) | (THead k0 u0 t2) \Rightarrow (THead k0 (lref_map
-f d0 u0) (lref_map f (s k0 d0) t2))]) in lref_map) (\lambda (x0: nat).(plus
-x0 (S O))) (s k d) t0)) | (TLRef _) \Rightarrow (THead k ((let rec lref_map
-(f: ((nat \to nat))) (d0: nat) (t1: T) on t1: T \def (match t1 with [(TSort
-n) \Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d0)
-with [true \Rightarrow i | false \Rightarrow (f i)])) | (THead k0 u0 t2)
-\Rightarrow (THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2))]) in
-lref_map) (\lambda (x0: nat).(plus x0 (S O))) d t) ((let rec lref_map (f:
-((nat \to nat))) (d0: nat) (t1: T) on t1: T \def (match t1 with [(TSort n)
-\Rightarrow (TSort n) | (TLRef i) \Rightarrow (TLRef (match (blt i d0) with
-[true \Rightarrow i | false \Rightarrow (f i)])) | (THead k0 u0 t2)
-\Rightarrow (THead k0 (lref_map f d0 u0) (lref_map f (s k0 d0) t2))]) in
-lref_map) (\lambda (x0: nat).(plus x0 (S O))) (s k d) t0)) | (THead _ _ t1)
-\Rightarrow t1])) (THead (Bind b) u (lift (S O) d (THead k t t0))) (THead k t
-t0) H1) in (\lambda (_: (eq T u t)).(\lambda (H6: (eq K (Bind b) k)).(let H7
-\def (eq_ind_r K k (\lambda (k0: K).(eq T (lift (S O) d (THead k0 t t0)) t0))
-H4 (Bind b) H6) in (let H8 \def (eq_ind T (lift (S O) d (THead (Bind b) t
-t0)) (\lambda (t1: T).(eq T t1 t0)) H7 (THead (Bind b) (lift (S O) d t) (lift
-(S O) (S d) t0)) (lift_bind b t t0 (S O) d)) in (H0 (lift (S O) d t) (S d) H8
-P)))))) H3)) H2))))))))))) x)).
-(* COMMENTS
-Initial nodes: 935
-END *)
+(\forall (P: Prop).P))))) in (let TMP_9 \def (\lambda (n: nat).(\lambda (u:
+T).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind b) u (lift (S O) d
+(TSort n))) (TSort n))).(\lambda (P: Prop).(let TMP_2 \def (Bind b) in (let
+TMP_3 \def (S O) in (let TMP_4 \def (TSort n) in (let TMP_5 \def (lift TMP_3
+d TMP_4) in (let TMP_6 \def (THead TMP_2 u TMP_5) in (let TMP_7 \def (\lambda
+(ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow
+False | (THead _ _ _) \Rightarrow True])) in (let TMP_8 \def (TSort n) in
+(let H0 \def (eq_ind T TMP_6 TMP_7 I TMP_8 H) in (False_ind P
+H0)))))))))))))) in (let TMP_17 \def (\lambda (n: nat).(\lambda (u:
+T).(\lambda (d: nat).(\lambda (H: (eq T (THead (Bind b) u (lift (S O) d
+(TLRef n))) (TLRef n))).(\lambda (P: Prop).(let TMP_10 \def (Bind b) in (let
+TMP_11 \def (S O) in (let TMP_12 \def (TLRef n) in (let TMP_13 \def (lift
+TMP_11 d TMP_12) in (let TMP_14 \def (THead TMP_10 u TMP_13) in (let TMP_15
+\def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) in (let TMP_16 \def
+(TLRef n) in (let H0 \def (eq_ind T TMP_14 TMP_15 I TMP_16 H) in (False_ind P
+H0)))))))))))))) in (let TMP_97 \def (\lambda (k: K).(\lambda (t: T).(\lambda
+(_: ((\forall (u: T).(\forall (d: nat).((eq T (THead (Bind b) u (lift (S O) d
+t)) t) \to (\forall (P: Prop).P)))))).(\lambda (t0: T).(\lambda (H0:
+((\forall (u: T).(\forall (d: nat).((eq T (THead (Bind b) u (lift (S O) d
+t0)) t0) \to (\forall (P: Prop).P)))))).(\lambda (u: T).(\lambda (d:
+nat).(\lambda (H1: (eq T (THead (Bind b) u (lift (S O) d (THead k t t0)))
+(THead k t t0))).(\lambda (P: Prop).(let TMP_18 \def (\lambda (e: T).(match e
+with [(TSort _) \Rightarrow (Bind b) | (TLRef _) \Rightarrow (Bind b) |
+(THead k0 _ _) \Rightarrow k0])) in (let TMP_19 \def (Bind b) in (let TMP_20
+\def (S O) in (let TMP_21 \def (THead k t t0) in (let TMP_22 \def (lift
+TMP_20 d TMP_21) in (let TMP_23 \def (THead TMP_19 u TMP_22) in (let TMP_24
+\def (THead k t t0) in (let H2 \def (f_equal T K TMP_18 TMP_23 TMP_24 H1) in
+(let TMP_25 \def (\lambda (e: T).(match e with [(TSort _) \Rightarrow u |
+(TLRef _) \Rightarrow u | (THead _ t1 _) \Rightarrow t1])) in (let TMP_26
+\def (Bind b) in (let TMP_27 \def (S O) in (let TMP_28 \def (THead k t t0) in
+(let TMP_29 \def (lift TMP_27 d TMP_28) in (let TMP_30 \def (THead TMP_26 u
+TMP_29) in (let TMP_31 \def (THead k t t0) in (let H3 \def (f_equal T T
+TMP_25 TMP_30 TMP_31 H1) in (let TMP_66 \def (\lambda (e: T).(match e with
+[(TSort _) \Rightarrow (let TMP_55 \def (\lambda (x0: nat).(let TMP_54 \def
+(S O) in (plus x0 TMP_54))) in (let TMP_56 \def (lref_map TMP_55 d t) in (let
+TMP_63 \def (\lambda (x0: nat).(let TMP_62 \def (S O) in (plus x0 TMP_62)))
+in (let TMP_64 \def (s k d) in (let TMP_65 \def (lref_map TMP_63 TMP_64 t0)
+in (THead k TMP_56 TMP_65)))))) | (TLRef _) \Rightarrow (let TMP_38 \def
+(\lambda (x0: nat).(let TMP_37 \def (S O) in (plus x0 TMP_37))) in (let
+TMP_39 \def (lref_map TMP_38 d t) in (let TMP_46 \def (\lambda (x0: nat).(let
+TMP_45 \def (S O) in (plus x0 TMP_45))) in (let TMP_47 \def (s k d) in (let
+TMP_48 \def (lref_map TMP_46 TMP_47 t0) in (THead k TMP_39 TMP_48)))))) |
+(THead _ _ t1) \Rightarrow t1])) in (let TMP_67 \def (Bind b) in (let TMP_68
+\def (S O) in (let TMP_69 \def (THead k t t0) in (let TMP_70 \def (lift
+TMP_68 d TMP_69) in (let TMP_71 \def (THead TMP_67 u TMP_70) in (let TMP_72
+\def (THead k t t0) in (let H4 \def (f_equal T T TMP_66 TMP_71 TMP_72 H1) in
+(let TMP_95 \def (\lambda (_: (eq T u t)).(\lambda (H6: (eq K (Bind b)
+k)).(let TMP_76 \def (\lambda (k0: K).(let TMP_73 \def (S O) in (let TMP_74
+\def (THead k0 t t0) in (let TMP_75 \def (lift TMP_73 d TMP_74) in (eq T
+TMP_75 t0))))) in (let TMP_77 \def (Bind b) in (let H7 \def (eq_ind_r K k
+TMP_76 H4 TMP_77 H6) in (let TMP_78 \def (S O) in (let TMP_79 \def (Bind b)
+in (let TMP_80 \def (THead TMP_79 t t0) in (let TMP_81 \def (lift TMP_78 d
+TMP_80) in (let TMP_82 \def (\lambda (t1: T).(eq T t1 t0)) in (let TMP_83
+\def (Bind b) in (let TMP_84 \def (S O) in (let TMP_85 \def (lift TMP_84 d t)
+in (let TMP_86 \def (S O) in (let TMP_87 \def (S d) in (let TMP_88 \def (lift
+TMP_86 TMP_87 t0) in (let TMP_89 \def (THead TMP_83 TMP_85 TMP_88) in (let
+TMP_90 \def (S O) in (let TMP_91 \def (lift_bind b t t0 TMP_90 d) in (let H8
+\def (eq_ind T TMP_81 TMP_82 H7 TMP_89 TMP_91) in (let TMP_92 \def (S O) in
+(let TMP_93 \def (lift TMP_92 d t) in (let TMP_94 \def (S d) in (H0 TMP_93
+TMP_94 H8 P)))))))))))))))))))))))) in (let TMP_96 \def (TMP_95 H3) in
+(TMP_96 H2)))))))))))))))))))))))))))))))))))) in (T_ind TMP_1 TMP_9 TMP_17
+TMP_97 x)))))).