pub fn while_rule_ty() -> Expr
WhileRule: {I ∧ b} C {I} ⊢ {I} while b do C {I ∧ ¬b}. Type: Prop → Prop → Prop