fact: Definition succb (alpha: t) : bool := match alpha with | inr (S _) | inl (S _) => true | _ => false end.
imports: Coq(Arith Compare_dec Lia) hydras(Comparable Simple_LexProd ON_Generic ON_plus ON_Omega Compat815)