Author: Not specified Language: text
Description: Not specified Timestamp: 2013-06-14 20:26:42 +0000
View raw paste Reply
  1. Inductive Plus_R : nat -> nat -> nat -> Type :=
  2. | Plus_O : forall m, Plus_R O m m
  3.    | Plus_S : forall m n r, Plus_R m n r -> Plus_R (S m) n (S r).
  4.  
View raw paste Reply