> That's not what I meant. Can x be a function, and can you then prove a proposition about x in a different module/in the same module in a different definition?

> That's not what I meant. Can x be a function, and can you then prove a proposition about x in a different module/in the same module in a different definition? Well, in my previous example I used an `int`, but there's no fundamental reason why you couldn't use a function (or any other type) instead. let f : list int -> list int = <mergesort> let p : (forall x. is_sorted (f x)) = <proof> In this example, `f` itself doesn't have a dependent type, and everything I want to prove about it is proved separately. But you can also do: let f : list (int * int) -> sorted_list (int * int) = <mergesort-sorting-by-first-int> let p : is_stable f = <proof-that-it-respects-the-relative-ordering-of-second-ints-amongst-entries-with-equal-first-ints> In this example, `f` contains a baked-in proof of one fact (that it sorts), but there's another fact that's proved separately (that it's stable). In general, the proof `p` needs access to the definition of `f`. So if `f` is held abstract (its definition isn't exposed to other modules), `p` has to be in the same module as `f`. In most programming languages, with respect to modularity, you only get two options: (0) Keep a value private. (Not expose it.) (1) Expose the existence of a value, indicating its type. Dependently typed languages give you a third option: (2) Expose the full definition of a value. As in, let developers of other modules know that `x` isn't just “a” function (or int or whatever) - it's this particular function (or int or whatever).