Function stable Copy item path

pub open spec fn stable<T>(temp_pred: TempPred<T>) -> TempPred<T>

{ temp_pred.implies(always(temp_pred)) }