The actual rule is more refined than that and doesn't prevent you from using constructors in the body or recursing without deconstructing any input, it just needs to prove the new inputs are "smaller" according to a fixed well-ordered relation. This is most often related to the structure of the input but is not required. For example I can have f(5) recurse into f(6) if that's "smaller" according to my custom relation, but no relation will allow me to continue increasing the argument forever.