implementation module DebugUtilities; // Auxillary functions E a b :== b; F s a :== a; FL s b :== b; FB b s b2 :== b2; FNONL s b :== b;