-nat).(\lambda (j: nat).(\lambda (H: (lt i j)).(le_S_n (S (S i)) (S j) (le_n_S
-(S (S i)) (S j) (le_n_S (S i) j H))))))) (\lambda (_: F).(\lambda (i:
-nat).(\lambda (j: nat).(\lambda (H: (lt i j)).H)))) k).
+nat).(\lambda (j: nat).(\lambda (H: (lt i j)).(le_n_S (S i) j H))))) (\lambda
+(_: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt i j)).H)))) k).