fact: Fixpoint succ (a : t) : t := match a with | nil => fin 1 | cons 0 n _ => cons 0 (S n) nil | cons a n b => cons a n (succ b) end.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )