fact: Fixpoint succ (a:T2) : T2 := match a with zero => one | gcons zero zero n c => fin (S (S n)) | gcons a b n c => gcons a b n (succ c) end.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)