[STATEMENT]
lemma all_LeadsTo_UN_UN:
     "\<forall>i. F \<in> (A i) LeadsTo (A' i)  
      ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. F \<in> A i \<longmapsto>w A' i \<Longrightarrow> F \<in> \<Union> (range A) \<longmapsto>w \<Union> (range A')
[PROOF STEP]
by (blast intro: LeadsTo_UN_UN)