Dear All, Is there any way to write inductive predicates in Mizar? My purpose is to have inductive predicates instead of recursive functions to avoid existence and uniqueness proofs of recursive functions and leaving the fact that this predicate has functional property as a later task. I have searched the library and could not find any examples. Thanks... Adem Ozyavas