[STATEMENT]
lemma ImplLeadsto_gen: "\<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> (F \<leadsto> G)
[PROOF STEP]
apply (unfold leadsto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<box>(Init F \<longrightarrow> Init G) \<longrightarrow> \<box>(Init F \<longrightarrow> \<diamond>G)
[PROOF STEP]
apply (auto intro!: InitDmd_gen [temp_use]
    elim!: STL4E_gen [temp_use] simp: Init_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done