pub fn seq_rule_ty() -> Expr
SeqRule: {P} C1 {R}, {R} C2 {Q} ⊢ {P} C1;C2 {Q}. Type: Prop → Prop → Prop → Prop