proposition: Remark rem2 : canon alpha (S i) = cons (T1.succ gamma) n (cons gamma i zero).
proof: Proof. subst alpha; now rewrite canonS_cons_succ_eqn2. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )