take NAT --> (1 succ 1) ; :: thesis: NAT --> (1 succ 1) is primitive-recursive
thus NAT --> (1 succ 1) is primitive-recursive ; :: thesis: verum