correct definedness side conditions for copy_apps and take_apps
handle case where copy_stricts cannot be proven; rewrite proof script for take_apps
rewrite proof script for take_stricts
remove redundant theorem attributes
add lemma iterate_below_fix
more precise dependencies;