section ‹Non-Recursive Algebraic Datatype› theory Sepref_Snip_Datatype imports "../../IICF/IICF" begin text ‹We define a non-recursive datatype›