implies_tla_exists_by_witness

vstd_extra::temporal_logic::rules

Function implies_tla_exists_by_witness 

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