add proof for nonzeros_app. if it were (say) nonfives, how would you destruct on (either 5 or not 5)? it's not a constructor