open Preamble open Core_notation