This merge request adds the lemma StronglySorted_app_iff (and the corollary StronglySorted_app), and rewrites the existing *_app lemmas as a corollary of StronglySorted_app_iff.
StronglySorted_app_iff
StronglySorted_app
*_app