proposition: Lemma mem_head_mult_inv : forall n h s, mem_head (hcons_mult h n s) -> h = head \/ mem_head s.
proof: Proof. induction n; cbn ; auto. inversion 1; auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )