fact: Fixpoint rough_unif (t1 t2 : term) {struct t1} : bool := match t1, t2 with | (Var _), _ => true | _, (Var _) => true | (Term f1 k1), (Term f2 k2) => if orb (is_def f1) (is_def f2) then true else if F.Symb.eq_bool f1 f2 then let rough_unif_list := (fix rough_unif_list (l1 l2 : list term) {struct l1} : bool := match l1, l2 with | nil, nil => true | nil, (_ :: _) => false | (_ :: _), nil => false | (t1 :: lt1), (t2 :: lt2) => andb (rough_unif t1 t2) (rough_unif_list lt1 lt2) end) in rough_unif_list k1 k2 else false end.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)