[STATEMENT]
lemma subterm_inj_on_alt_def:
    "subterm_inj_on f A \<longleftrightarrow>
     (inj_on f A \<and> (\<forall>s \<in> f`A. \<forall>u \<in> f`A. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u))"
    (is "?A \<longleftrightarrow> ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subterm_inj_on f A = (inj_on f A \<and> (\<forall>s\<in>f ` A. \<forall>u\<in>f ` A. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u))
[PROOF STEP]
unfolding subterm_inj_on_def inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A. \<forall>y\<in>A. (\<exists>v. v \<sqsubseteq> f x \<and> v \<sqsubseteq> f y) \<longrightarrow> x = y) = ((\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y) \<and> (\<forall>s\<in>f ` A. \<forall>u\<in>f ` A. (\<exists>v. v \<sqsubseteq> s \<and> v \<sqsubseteq> u) \<longrightarrow> s = u))
[PROOF STEP]
by fastforce