[STATEMENT]
lemma c_types_agree_top1: "c_types_agree (TopType []) ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_types_agree (TopType []) ts
[PROOF STEP]
using ct_suffix_ts_conv_suffix to_ct_list_def
[PROOF STATE]
proof (prove)
using this:
ct_suffix (to_ct_list ?ts) (to_ct_list ?ts') = suffix ?ts ?ts'
to_ct_list ?ts = map TSome ?ts

goal (1 subgoal):
 1. c_types_agree (TopType []) ts
[PROOF STEP]
by (simp add: ct_suffix_nil)