Function parallel_composition_rule_ty 

pub fn parallel_composition_rule_ty() -> Expr

ParallelCompositionRule: {P1} C1 {Q1}, {P2} C2 {Q2} ⊢ {P1∗P2} C1||C2 {Q1∗Q2}. Type: Prop