leads_to_tla_exists_by_witness

vstd_extra::temporal_logic::rules

Function leads_to_tla_exists_by_witness 

Source 
pub proof fn leads_to_tla_exists_by_witness<T, A>(
    spec: TempPred<T>,
    p: TempPred<T>,
    q: FnSpec<(A,), TempPred<T>>,
    a: A,
)
Expand description
requires
spec.entails(p.leads_to(q(a))),
ensures
spec.entails(p.leads_to(tla_exists(q))),