proposition: Lemma const_pathS_eps_trans : forall i alpha beta gamma, const_pathS_eps i alpha beta -> const_pathS_eps i beta gamma -> const_pathS_eps i alpha gamma .
proof: Proof. destruct 1. - destruct 1. + left; eapply const_pathS_trans; eauto. + subst; now left. - trivial. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)