\forall (k: K).(\forall (i: nat).(eq nat (minus (s k i) (s k O)) i))
\def
\lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (minus i O) (\lambda (n:
nat).(eq nat n i)) (eq_ind nat i (\lambda (n: nat).(eq nat n i)) (refl_equal
nat i) (minus i O) (minus_n_O i)) (minus (s k i) (s k O)) (minus_s_s k i O))).
\forall (k: K).(\forall (i: nat).(eq nat (minus (s k i) (s k O)) i))
\def
\lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (minus i O) (\lambda (n:
nat).(eq nat n i)) (eq_ind nat i (\lambda (n: nat).(eq nat n i)) (refl_equal
nat i) (minus i O) (minus_n_O i)) (minus (s k i) (s k O)) (minus_s_s k i O))).