proposition: Lemma FinS_Succ_eq : forall i, E0finS i = E0_succ (E0fin i).
proof: Proof. intro i; compute. orefl; now destruct i. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)