[STATEMENT]
lemma minsolD': "s \<in> g =\<^sub>M h \<Longrightarrow> s \<noteq> \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> g =\<^sub>M h \<Longrightarrow> s \<noteq> \<epsilon>
[PROOF STEP]
using minsoldef
[PROOF STATE]
proof (prove)
using this:
?s \<in> ?g =\<^sub>M ?h \<equiv> ?s \<noteq> \<epsilon> \<and> ?g ?s = ?h ?s \<and> (\<forall>s'. s' \<le>np ?s \<and> ?g s' = ?h s' \<longrightarrow> s' = ?s)

goal (1 subgoal):
 1. s \<in> g =\<^sub>M h \<Longrightarrow> s \<noteq> \<epsilon>
[PROOF STEP]
by blast