proposition: Lemma path_toS_trace alpha s beta : path_toS beta s alpha -> nf alpha -> trace_to (iota beta) s (iota alpha).
proof: Proof. induction 1. - destruct H. intro; left. subst. apply canonS_iota_i; auto. - intro. right with (iota gamma). destruct H. subst. apply canonS_iota_i; auto. apply IHpath_toS. destruct H. subst. apply nf_canon. auto. Qed.
imports: Coq(Relation_Operators) hydras(Hydra_Lemmas Epsilon0 Canon Paths )