nat_induction { 
  "Base Case": \add ( ==> {\subst nv; 0}(b) );
  "Step Case": \add ( ==> \forall nv; (nv >= 0 & b) ->
                                       {\subst nv; (nv + 1)}b));
  "Use Case":  \add ( \forall nv; (nv >= 0 -> b) ==>) 
};