fact: Fixpoint nbterms (t:T2) : nat := match t with zero => 0 | gcons a b n v => (S n) + nbterms v end.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)