[STATEMENT]
lemma minGraphProps7': "minGraphProps g \<Longrightarrow>
  f \<in> \<F> g \<Longrightarrow> v \<in> \<V> f \<Longrightarrow>  f \<in> set (faceListAt g ! v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f\<rbrakk> \<Longrightarrow> f \<in> set (faceListAt g ! v)
[PROOF STEP]
apply (frule minGraphProps7)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f\<rbrakk> \<Longrightarrow> ?f \<in> \<F> g
 2. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f\<rbrakk> \<Longrightarrow> ?v \<in> \<V> ?f
 3. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f; ?f \<in> set (facesAt g ?v)\<rbrakk> \<Longrightarrow> f \<in> set (faceListAt g ! v)
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>minGraphProps g; f \<in> \<F> g; v \<in> \<V> f; f \<in> set (facesAt g v)\<rbrakk> \<Longrightarrow> f \<in> set (faceListAt g ! v)
[PROOF STEP]
by (simp add: facesAt_def split: if_split_asm)