DEFINITION r_dis()
TYPE =
       ∀k:K
         .∀P:Prop
           .(∀i:nat.(eq nat (r k i) i))→P
             →((∀i:nat.(eq nat (r k i) (S i)))→P)→P
BODY =
Show proof