Function dependent_ghost::proof::such_that

pub fn such_that<A, P>(x: A, p: Proof<P>) -> SuchThat<A, P>

Annotate a value with a proof.