proposition: Lemma const_pathS_trans : forall n alpha beta gamma, const_path (S n) alpha beta -> const_path (S n) beta gamma -> const_path (S n) alpha gamma.
proof: Proof. intros *; repeat rewrite <- const_pathSE; unfold const_pathS; intros H H0; rewrite <- clos_trans_t1n_iff in *; constructor 2 with beta; assumption. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)