- \lambda (k: K).(let TMP_1 \def (\lambda (k0: K).(\forall (i: nat).(\forall
-(j: nat).((lt (s k0 i) (s k0 j)) \to (lt i j))))) in (let TMP_3 \def (\lambda
-(b: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt (s (Bind b) i) (s
-(Bind b) j))).(let TMP_2 \def (S i) in (le_S_n TMP_2 j H)))))) in (let TMP_4
-\def (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt (s
-(Flat f) i) (s (Flat f) j))).H)))) in (K_ind TMP_1 TMP_3 TMP_4 k)))).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j:
+nat).((lt (s k0 i) (s k0 j)) \to (lt i j))))) (\lambda (b: B).(\lambda (i:
+nat).(\lambda (j: nat).(\lambda (H: (lt (s (Bind b) i) (s (Bind b)
+j))).(le_S_n (S i) j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j:
+nat).(\lambda (H: (lt (s (Flat f) i) (s (Flat f) j))).H)))) k).