proposition: Lemma path_to_not_In_zero : forall alpha s beta, path_to beta s alpha -> ~ In 0 s.
proof: Proof. induction 1. - red; destruct 1. + contradiction. + destruct H1. - intro H2; destruct H2; contradiction. Qed.
imports: hydras(DecPreOrder Canon MoreLists First_toggle OrdNotations) Coq(Lia)