implies_tla_exists_intro

vstd_extra::temporal_logic::rules

Function implies_tla_exists_intro 

Source 
pub broadcast proof fn implies_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.implies(q(a))),
ensures
#[trigger] spec.entails(p.implies(tla_exists(q))),