proposition: Remark rem3 : iota (canon alpha (S i)) = node (hy_app (hcons_mult (iota (T1.succ gamma)) (S n) hnil) (hcons_mult (iota gamma) (S i) hnil)).
proof: Proof. rewrite rem2; simpl; rewrite (iota_of_succ gamma); [| trivial]. - case_eq (iota gamma). + intros; rewrite <- hcons_mult_comm; f_equal. rewrite <- hcons_mult_app; simpl; rewrite hcons_mult_comm; f_equal. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )