[STATEMENT]
lemma proper_it'I:
    "\<lbrakk>\<And>s. proper_it (it s) (it' s)\<rbrakk> \<Longrightarrow> proper_it' it it'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. proper_it (it s) (it' s)) \<Longrightarrow> proper_it' it it'
[PROOF STEP]
unfolding proper_it'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. proper_it (it s) (it' s)) \<Longrightarrow> \<forall>s. proper_it (it s) (it' s)
[PROOF STEP]
by blast