pub open spec fn valid<T>(temp_pred: TempPred<T>) -> bool
{ forall |ex: Execution<T>| temp_pred.satisfied_by(ex) }