[STATEMENT]
lemma rt_fresher_single [intro]:
  assumes "rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2"
    shows "the (rt1 ip) \<sqsubseteq> the (rt2 ip)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rt1 \<sqsubseteq>\<^bsub>ip\<^esub> rt2

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
unfolding rt_fresher_def
[PROOF STATE]
proof (prove)
using this:
the (rt1 ip) \<sqsubseteq> the (rt2 ip)

goal (1 subgoal):
 1. the (rt1 ip) \<sqsubseteq> the (rt2 ip)
[PROOF STEP]
.