Function prop::path_semantics::comp

pub fn comp<F1: Prop, F2: Prop, F3: Prop, F4: Prop, X1: Prop, X2: Prop>(
    f: PSem<F1, F2, F3, F4>, 
    g: PSem<F3, F4, X1, X2>, 
    pr_f1_f3: POrdProof<F1, F3>, 
    pr_f2_f4: POrdProof<F2, F4>, 
    pr_f3_x1: POrdProof<F3, X1>, 
    pr_f4_x2: POrdProof<F4, X2>, 
    f1_f3: Imply<F1, F3>, 
    f2_f4: Imply<F2, F4>, 
    f3_x1: Imply<F3, X1>, 
    f4_x2: Imply<F4, X2>
) -> PSem<F1, F2, X1, X2>

Composition.