- \lambda (k: K).(let TMP_2 \def (\lambda (k0: K).(\forall (i: nat).(let TMP_1
-\def (s k0 i) in (le i TMP_1)))) in (let TMP_30 \def (\lambda (b: B).(\lambda
-(i: nat).(let TMP_3 \def (Bind b) in (let TMP_4 \def (s TMP_3 i) in (let
-TMP_5 \def (S i) in (let TMP_6 \def (Bind b) in (let TMP_7 \def (s TMP_6 i)
-in (let TMP_8 \def (S TMP_7) in (let TMP_9 \def (S i) in (let TMP_10 \def (S
-TMP_9) in (let TMP_11 \def (Bind b) in (let TMP_12 \def (s TMP_11 i) in (let
-TMP_13 \def (S TMP_12) in (let TMP_14 \def (S TMP_13) in (let TMP_15 \def (S
-i) in (let TMP_16 \def (S TMP_15) in (let TMP_17 \def (S TMP_16) in (let
-TMP_18 \def (Bind b) in (let TMP_19 \def (s TMP_18 i) in (let TMP_20 \def (S
-TMP_19) in (let TMP_21 \def (S TMP_20) in (let TMP_22 \def (Bind b) in (let
-TMP_23 \def (s TMP_22 i) in (let TMP_24 \def (S TMP_23) in (let TMP_25 \def
-(S TMP_24) in (let TMP_26 \def (le_n TMP_25) in (let TMP_27 \def (le_S TMP_17
-TMP_21 TMP_26) in (let TMP_28 \def (le_S_n TMP_10 TMP_14 TMP_27) in (let
-TMP_29 \def (le_S_n TMP_5 TMP_8 TMP_28) in (le_S_n i TMP_4
-TMP_29)))))))))))))))))))))))))))))) in (let TMP_33 \def (\lambda (f:
-F).(\lambda (i: nat).(let TMP_31 \def (Flat f) in (let TMP_32 \def (s TMP_31
-i) in (le_n TMP_32))))) in (K_ind TMP_2 TMP_30 TMP_33 k)))).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(le i (s k0 i))))
+(\lambda (b: B).(\lambda (i: nat).(le_S_n i (s (Bind b) i) (le_S_n (S i) (S
+(s (Bind b) i)) (le_S_n (S (S i)) (S (S (s (Bind b) i))) (le_S (S (S (S i)))
+(S (S (s (Bind b) i))) (le_n (S (S (s (Bind b) i)))))))))) (\lambda (f:
+F).(\lambda (i: nat).(le_n (s (Flat f) i)))) k).