return to top
source
This module proves the stated slice and evolution properties used by the ESS formalization.