The first attempt to implement supercompilaton by reflection/normalization in Agda (very simple unfolding of bool eliminator is implemented)