proposition: Lemma trace_to_round_plus h' : forall t h, trace_to h' t h -> round_plus h h'.
proof: Proof. induction 1. - left; exists n; auto. - right with h'0. exists n; auto. apply IHtrace_to. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )