Function lift_state_exists Copy item path

pub open spec fn lift_state_exists<T, A>(
    a_to_state_pred: FnSpec<(A,), StatePred<T>>,
) -> TempPred<T>

{ lift_state(StatePred::state_exists(a_to_state_pred)) }