proposition: Lemma R12_reg : forall s t : term, @union term R1 R2 s t -> forall x : variable, In x (var_list s) -> In x (var_list t).
proof: Proof. intros s t [H1 | H2] x x_in_s. apply R1_reg with s; trivial. apply R2_reg with s; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)