proposition: Lemma R1_R2 : forall h h', R1 h h' -> R2 0 (hyd1 h) (hyd1 h').
proof: Proof. intros; destruct h, h'; left; change (hcons (node h0) hnil) with (hcons_mult (node h0) 1 hnil); now left. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )