proposition: Lemma def_dec12 : forall f : symbol, {defined (@union _ R1 R2) f} + {~ defined (@union _ R1 R2) f}.
proof: Proof. intro f; destruct (def_dec1 f) as [D1f | C1f]. left; inversion D1f as [f' k t H1]; subst f'. refine (Def _ f k t _); left; trivial. destruct (def_dec2 f) as [D2f | C2f]. left; inversion D2f as [f' k t H1]; subst f'. refine (Def _ f k t _); right; trivial. right; intros Df; inversion Df as [f' k t [H1 | H2]]; subst f'. apply C1f; apply (Def _ _ _ _ H1). apply C2f; apply (Def _ _ _ _ H2). Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)