[STATEMENT]
lemma Agent_univ: "(UNIV :: Agent set) = {Robot}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = {Robot}
[PROOF STEP]
unfolding UNIV_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_ext (\<lambda>x. True) = {Robot}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Robot
[PROOF STEP]
apply (case_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x = Robot \<Longrightarrow> x = Robot
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done