fact: Definition equiv_bool_F := (fun (equiv_bool : term -> term -> bool) (t1 t2 : term) => match t1, t2 with | Var v1, Var v2 => X.eq_bool v1 v2 | Var _, Term _ _ => false | Term _ _, Var _ => false | Term f1 l1, Term f2 l2 => if prec_eq_bool Prec f1 f2 then match status Prec f1 with | Lex => let equiv_lex_bool := (fix equiv_lex_bool (kk1 kk2 : list term) {struct kk1} : bool := (match kk1 with | [] => match kk2 with [] => true | _ :: _=> false end | t1 :: k1 => match kk2 with [] => false | t2 :: k2=> (equiv_bool t1 t2) && (equiv_lex_bool k1 k2) end end)) in (equiv_lex_bool l1 l2) | Mul => let equiv_mult_bool := (fix equiv_mult_bool (kk1 kk2 : list term) {struct kk1} : bool := (match kk1 with | [] => match kk2 with [] => true | _ :: _=> false end | t1 :: k1 => match remove equiv_bool t1 kk2 with None => false | Some k2 => equiv_mult_bool k1 k2 end end)) in (equiv_mult_bool l1 l2) end else false end) : (term -> term -> bool) -> term -> term -> bool.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)