[STATEMENT]
lemma ineffectual_const_get:
  "\<exists> v.  \<forall> \<sigma>\<in>\<S>. get \<sigma> = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. \<forall>\<sigma>\<in>\<S>. get \<sigma> = v
[PROOF STEP]
using put_get put_inef
[PROOF STATE]
proof (prove)
using this:
get (put ?\<sigma> ?v) = ?v
put ?\<sigma> ?v = ?\<sigma>

goal (1 subgoal):
 1. \<exists>v. \<forall>\<sigma>\<in>\<S>. get \<sigma> = v
[PROOF STEP]
by auto