proposition: Lemma trace_to_std_0 h' : forall l i h, trace_to h' (iota_from i (S l)) h -> rounds standard i h (S l + i) h'.
proof: Proof. induction l. simpl. intros. left. red. simpl. inversion H. auto. inversion H4. intros. inversion H. subst. right with h'0. simpl. auto. specialize (IHl (S i) h'0 H4). simpl. rewrite Nat.add_succ_r in IHl. auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )