DEFINITION r_plus_sym()
TYPE =
       ∀k:K.∀i:nat.∀j:nat.(eq nat (r k (plus i j)) (plus i (r k j)))
BODY =
Show proof