pub fn wp_completeness_ty() -> Expr
WPCompleteness: if {P} C {Q} then P ⊢ wp(C, Q). Type: {P Q : Prop} → {C : Program} → HoareTriple P C Q → Prop