proposition: Lemma R12_var : forall (v : variable) (t :term), ~ (@union _ R1 R2) t (Var v).
proof: Proof. intros v u [H1 | H2]. apply (R1_var _ _ H1). apply (R2_var _ _ H2). Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)