inductive add (p:nat): nat \to nat \to Prop \def
| add_O_2: add p O p
| add_S_2: \forall q, r. add p q r \to add p (S q) (S r).
inductive add (p:nat): nat \to nat \to Prop \def
| add_O_2: add p O p
| add_S_2: \forall q, r. add p q r \to add p (S q) (S r).