[STATEMENT]
theorem sup_PTS_eq:
  "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G \<turnstile> OK (PrimT p) <=o X = (X = Err \<or> X = OK (PrimT p))
[PROOF STEP]
by (auto simp add: sup_ty_opt_def Err.le_def lesub_def subtype_def 
              split: err.splits)