Type Alias DepFun 

pub type DepFun<F, A, X, PredP> = Ty<F, DepFunTy<A, X, PredP>>;

Dependent function f : ((a : x) -> p(a)).