fact: Fixpoint T2_size (o:T2):nat := match o with zero => 0 | gcons a b n c => S (T2_size a + T2_size b + n + T2_size c)%nat end.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)