Function lift_state_forall_absorb_equality

pub broadcast proof fn lift_state_forall_absorb_equality<T, A>(
    a_to_state_pred: FnSpec<(A,), StatePred<T>>,
    state_pred: StatePred<T>,
)

Expand description

requires

Set::<A>::full() != Set::<A>::empty(),

ensures

#[trigger] lift_state_forall(a_to_state_pred).and(lift_state(state_pred))
    == lift_state_forall(StatePred::absorb(a_to_state_pred, state_pred)),

lift_state_forall_absorb_equality