proposition: Remark all_cases : exists beta n gamma, nf beta /\ nf gamma /\ alpha = cons beta n gamma.
proof: Proof. destruct alpha as [| beta n gamma]. - destruct nonzero; auto. - exists beta, n, gamma; split;eauto with T1. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )