leads_to_tla_exists_intro

vstd_extra::temporal_logic::rules

Function leads_to_tla_exists_intro 

Source 
pub broadcast proof fn leads_to_tla_exists_intro<T, A>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: FnSpec<(A,), TempPred<T>>,
)
Expand description
requires
exists |a: A| #[trigger] spec.entails(p.leads_to(q(a))),
ensures
#[trigger] spec.entails(p.leads_to(tla_exists(q))),