Failed to apply initial proof method⌂:
using this:
  [] ∈ ns_public
goal (1 subgoal):
 1. ∀A B X. Says A B X ∉ set_of_list []

inductive_set ns_public :: "event list set"
where
  Nil[intro!,simp] : "[] ∈ ns_public"  |

....
<snip>
....

lemma "∀ A B X. [] ∈ ns_public ⟶ Says A B X ∉ set_of_list []"
proof
  assume "[] ∈ ns_public"
  from this have  "∀ A B X. Says A B X ∉ set_of_list []"
  from this show "True" by blast
oops