Function prop::path_semantics::ty_in_right_arg

pub fn ty_in_right_arg<A: Prop, B: Prop, C: Prop>(
    (ab, pord): Ty<A, B>, 
    eq: Eq<B, C>
) -> Ty<A, C>

(a : b) ⋀ (b == c) => (a : c).