pub fn termination_proof_ty() -> Expr
TerminationProof: a proof that program C terminates from every state satisfying P. Type: Prop → Program → Prop