[STATEMENT]
lemma OUTfromChCorrect_data8: "OUTfromChCorrect data8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OUTfromChCorrect data8
[PROOF STEP]
by (simp add: OUTfromChCorrect_def, metis IN.simps(18) OUT.simps(18) insertI1)