Function prop::path_semantics::uniq_ty

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

Proves that types are unique.