Function fun_type0 

pub fn fun_type0<A: Prop, B: Prop, N: Nat, M: Nat>(
    ty_a: Ty<A, Type<N>>,
    ty_b: Ty<B, Type<M>>,
) -> Ty<Pow<B, A>, Type<Z>>

(a : type(n)) ⋀ (b : type(m)) => (a -> b) : type(0).