proposition: Lemma Successor_inv4 : forall i j, ~ Successor (inl j) (inr i).
proof: Proof. destruct 1 as [H H0]; inversion H. Qed.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)