proposition: Lemma R1_hcons : forall h s1 s2, R1 (node s1) (node s2) -> R1 (node (hcons h s1)) (node (hcons h s2)).
proof: Proof. inversion 1;split;now right. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )