entails_tla_exists_by_witness

vstd_extra::temporal_logic::rules

Function entails_tla_exists_by_witness 

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