[STATEMENT]
lemma DNI_CoP1: "Fr_1b \<F> \<Longrightarrow> DNI \<^bold>\<not> \<Longrightarrow> CoP1 \<^bold>\<not>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Fr_1b \<F>; DNI \<^bold>\<not>\<rbrakk> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
using CoP1_def2 CoPw
[PROOF STATE]
proof (prove)
using this:
CoP1 ?\<eta> = (CoPw ?\<eta> \<and> DNI ?\<eta>)
Fr_1b \<F> \<Longrightarrow> CoPw \<^bold>\<not>

goal (1 subgoal):
 1. \<lbrakk>Fr_1b \<F>; DNI \<^bold>\<not>\<rbrakk> \<Longrightarrow> CoP1 \<^bold>\<not>
[PROOF STEP]
by blast