pub fn consequence_rule_ty() -> Expr
ConsequenceRule: P ⊢ P’, {P’} C {Q’}, Q’ ⊢ Q ⊢ {P} C {Q}. Type: Prop