proposition: Lemma no_need_of_instance_is_modular : forall (R1 R2 : term -> term -> Prop), (forall t1 t2, axiom R1 t1 t2 -> R1 t1 t2) -> (forall t1 t2, axiom R2 t1 t2 -> R2 t1 t2) -> (forall t1 t2, axiom (union term R1 R2) t1 t2 -> (union term R1 R2) t1 t2).
proof: Proof. intros R1 R2 H1 H2 t1 t2 H; inversion H as [t1' t2' sigma H']; subst; inversion H'; [left; apply H1 | right; apply H2]; apply instance; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)