[STATEMENT]
lemma at_neg_neg2:"\<Turnstile>\<^bold>\<not>(\<^bold>@c \<^bold>\<not> \<phi>) \<^bold>\<rightarrow> (\<^bold>@c  \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ts v. \<not> (\<forall>v'. v = c > v' \<longrightarrow> \<not> \<phi> ts v') \<longrightarrow> (\<forall>v'. v = c > v' \<longrightarrow> \<phi> ts v')
[PROOF STEP]
using switch_unique switch_def switch_refl
[PROOF STATE]
proof (prove)
using this:
?v = ?c > ?u \<and> ?v = ?c > ?w \<longrightarrow> ?u = ?w
?v = ?c > ?w \<equiv> ext ?v = ext ?w \<and> lan ?v = lan ?w \<and> own ?w = ?c \<and> more ?v = more ?w
?v = own ?v > ?v

goal (1 subgoal):
 1. \<forall>ts v. \<not> (\<forall>v'. v = c > v' \<longrightarrow> \<not> \<phi> ts v') \<longrightarrow> (\<forall>v'. v = c > v' \<longrightarrow> \<phi> ts v')
[PROOF STEP]
by metis