nat).((lt i j) \to (lt (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i:
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).
nat).((lt i j) \to (lt (s k0 i) (s k0 j)))))) (\lambda (_: B).(\lambda (i:
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).