lift_state_exists_leads_to_intro

vstd_extra::temporal_logic::rules

Function lift_state_exists_leads_to_intro 

Source 
pub broadcast proof fn lift_state_exists_leads_to_intro<T, A>(
    spec: TempPred<T>,
    a_to_temp_pred: FnSpec<(A,), StatePred<T>>,
    q: TempPred<T>,
)
Expand description
requires
forall |a: A| #[trigger] spec.entails(lift_state(a_to_temp_pred(a)).leads_to(q)),
ensures
#[trigger] spec.entails(lift_state_exists(a_to_temp_pred).leads_to(q)),