[STATEMENT]
lemma at_res1:"\<Turnstile>(re(c)) \<^bold>\<rightarrow> (\<^bold>\<forall>d. \<^bold>@d re(c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>ts v. 0 < \<parallel>ext v\<parallel> \<and> len v ts c = ext v \<and> restrict v (res ts) c = lan v \<and> |lan v| = 1 \<longrightarrow> (\<forall>x v'. v = x > v' \<longrightarrow> 0 < \<parallel>ext v'\<parallel> \<and> len v' ts c = ext v' \<and> restrict v' (res ts) c = lan v' \<and> |lan v'| = 1)
[PROOF STEP]
by (metis (no_types, lifting) perfect_sensors.switch_length_stable 
      restriction.switch_restrict_stable view.switch_def)