pub fn ranking_function_ty() -> Expr
RankingFunction: a function from states to a well-founded set, decreasing on each loop iteration. Type: {S : Type} → (S → Nat) → Program → Prop