state_pred_implies_apply_equality

vstd_extra::temporal_logic::rules

Function state_pred_implies_apply_equality 

Source 
pub broadcast proof fn state_pred_implies_apply_equality<T>(
    p: StatePred<T>,
    q: StatePred<T>,
    s: T,
)
Expand description
ensures
#[trigger] p.implies(q).apply(s) == (p.apply(s) ==> q.apply(s)),

Lift StatePred::implies to Verus meta-level.