header {* Main includes everything *} theory Main imports CTT Arith Bool begin end