proposition: Lemma acc_from_trans : forall alpha beta gamma, acc_from alpha beta -> acc_from beta gamma -> acc_from alpha gamma.
proof: Proof. destruct 1 as [s1 H1]. destruct 1 as [s2 H2]. exists (s1 ++ s2). now apply path_to_app with beta. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)