Function lift_state_forall Copy item path

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

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