state_exists_intro

vstd_extra::temporal_logic::rules

Function state_exists_intro 

Source 
pub broadcast proof fn state_exists_intro<T, A>(
    a_to_temp_pred: FnSpec<(A,), StatePred<T>>,
    s: T,
)
Expand description
requires
exists |a: A| #[trigger] a_to_temp_pred(a).apply(s),
ensures
#[trigger] StatePred::state_exists(a_to_temp_pred).apply(s),