preservation and progress proven
with correct cast rule and accordingly modified compability for functions.