lift_state_exists_absorb_equality

vstd_extra::temporal_logic::rules

Function lift_state_exists_absorb_equality 

Source 
pub broadcast proof fn lift_state_exists_absorb_equality<T, A>(
    a_to_state_pred: FnSpec<(A,), StatePred<T>>,
    state_pred: StatePred<T>,
)
Expand description
ensures
#[trigger] lift_state_exists(a_to_state_pred).and(lift_state(state_pred))
    == lift_state_exists(StatePred::absorb(a_to_state_pred, state_pred)),