fact: Fixpoint eq_bool (t1 t2 :term) : bool := match t1, t2 with | Var v1, Var v2 => eq_var_bool v1 v2 | Var _, Term _ _ => false | Term _ _, Var _ => false | Term f1 l1, Term f2 l2 => if eq_symb_bool f1 f2 then let eq_bool_list := (fix eq_bool_list (l1 l2: list term) {struct l1} : bool := match l1, l2 with | nil, nil => true | nil, (_ :: _) => false | (_::_), nil => false | t1 :: k1, t2 :: k2 => andb (eq_bool t1 t2) (eq_bool_list k1 k2) end) in eq_bool_list l1 l2 else false end.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set)