Functional Programming, Formal Methods.
two slightly different ways, one “simple” (CNat) and one “inductive” (INat). The later view refers to the former, so, there is no mutual recursion involved. Plus, since INat is a predicate on CNat, it has an n in scope, so it can return P n. Both implementations are then “merged together” in a last