[STATEMENT]
lemma fresher_refl [simp]: "r \<sqsubseteq> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<sqsubseteq> r
[PROOF STEP]
unfolding fresher_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nsqn\<^sub>r r < nsqn\<^sub>r r \<or> nsqn\<^sub>r r = nsqn\<^sub>r r \<and> \<pi>\<^sub>5 r \<le> \<pi>\<^sub>5 r
[PROOF STEP]
by simp