always_double_equality

vstd_extra::temporal_logic::rules

Function always_double_equality 

Source 
pub broadcast proof fn always_double_equality<T>(p: TempPred<T>)
Expand description
ensures
#[trigger] always(always(p)) == always(p),

Double □ can be simplified.

§Postconditions

  • □□p == □p