proposition: Lemma def_dec3' : forall f : symbol, {defined (@union _ R3 (Pi pi V0 V1)) f} + {~ defined (@union _ R3 (Pi pi V0 V1)) f}.
proof: Proof. intros f; destruct (def_dec3 f) as [Df | Cf]. left; inversion Df as [f' l s H]; subst. apply (Def (@union _ R3 (Pi pi V0 V1)) f l s); left; trivial. generalize (F.Symb.eq_bool_ok f pi); case (F.Symb.eq_bool f pi); [intros f_eq_pi | intros f_diff_pi]. subst f; left; apply (Def (@union _ R3 (Pi pi V0 V1)) pi (Var V0 :: Var V1 :: nil) (Var V0)). right; apply Pi1. right; intro Df; inversion Df as [f' l s [H3 | Hpi]]; subst. apply Cf; apply (Def R3 f l s); trivial. inversion Hpi; subst f; absurd (pi = pi); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)