proposition: Lemma rough_unif_unfold : forall t1 t2, rough_unif t1 t2 = 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 rough_unif_list k1 k2 else false end.
proof: Proof. intros t1 t2; destruct t1 as [v1 | f1 k1]. apply eq_refl. destruct t2 as [v2 | f2 k2]. apply eq_refl. simpl; destruct (is_def f1). apply eq_refl. destruct (is_def f2). apply eq_refl. destruct (eq_symb_bool f1 f2); [simpl | apply eq_refl]. revert k2; induction k1 as [ | t1 k1]; intros [ | t2 k2]; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)