fact: Fixpoint 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.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)