pub broadcast proof fn tla_forall_apply<T, A>(a_to_temp_pred: FnSpec<(A,), TempPred<T>>, a: A)Expand description
ensures
#[trigger] tla_forall(a_to_temp_pred).entails(a_to_temp_pred(a)),If forall a. P(a) holds, then P holds for any particular a.
§Postconditions
∀ a: A. P(a) ⊧ P(a)