[STATEMENT]
lemma leadsTo_Union: 
    "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. A \<in> S \<Longrightarrow> F \<in> A \<longmapsto> B) \<Longrightarrow> F \<in> \<Union> S \<longmapsto> B
[PROOF STEP]
apply (unfold leadsTo_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. A \<in> S \<Longrightarrow> F \<in> {F. (A, B) \<in> leads F}) \<Longrightarrow> F \<in> {F. (\<Union> S, B) \<in> leads F}
[PROOF STEP]
apply (blast intro: leads.Union)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done