proposition: Lemma R1_hcons_mult : forall n h s1 s2, R1 (node s1) (node s2) -> R1 (node (hcons_mult h n s1)) (node (hcons_mult h n s2)).
proof: Proof. inversion 1; split; now apply hcons_mult_S0. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )