[STATEMENT]
lemma iprop11a': "Fr_1 \<F> \<Longrightarrow> \<forall>a b. (a \<^bold>\<Rightarrow> (a \<^bold>\<Rightarrow> b)) \<^bold>\<preceq> (a \<^bold>\<Rightarrow> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_1 \<F> \<Longrightarrow> \<forall>a b. contains (b \<^bold>\<Leftarrow> a) ((b \<^bold>\<Leftarrow> a) \<^bold>\<Leftarrow> a)
[PROOF STEP]
by (smt MONO_def PF1 imp_rel monI conn)