fact: Fixpoint compare (u v: T) := match u,v with | sum i l, sum j vs => lex (idx_compare i j) (mset_compare compare l vs) | prd i l, prd j vs => lex (idx_compare i j) (list_compare compare l vs) | sym i l, sym j vs => lex (idx_compare i j) (vcompare l vs) | unit i , unit j => idx_compare i j | unit _ , _ => Lt | _ , unit _ => Gt | sum _ _, _ => Lt | _ , sum _ _ => Gt | prd _ _, _ => Lt | _ , prd _ _ => Gt end with vcompare i j (us: vT i) (vs: vT j) := match us,vs with | vnil, vnil => Eq | vnil, _ => Lt | _, vnil => Gt | vcons _ u us, vcons _ v vs => lex (compare u v) (vcompare us vs) end.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)