Function prop::path_semantics::uniq_ty

pub fn uniq_ty<A: Prop, B: Prop, C: Prop, D: Prop, E: Prop>(
    eq_a_b: Eq<A, B>, 
    f: Imply<A, And<C, D>>, 
    b_e: Imply<B, E>, 
    p_a: PSem<A, B, C, E>, 
    p_b: PSem<A, B, D, E>
) -> Eq<C, D>

Proves that types are unique.