proposition: Lemma Bigstep : forall b i a , reachable i a b 0 -> reachable (iterate doubleS b i) a 0 0.
proof: Proof. induction b. - trivial. - intros; simpl; apply reachable_S in H. rewrite <- iterate_comm; now apply IHb. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)