proposition: Lemma standard_path_zero : forall i j alpha beta, standard_path i alpha j beta -> alpha = zero -> beta = zero.
proof: Proof. induction 1. - intro; subst; now rewrite canon_zero. - intro; subst; rewrite canon_zero in IHstandard_path_to; auto. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)