proposition: Lemma def_dec123' : forall f : symbol, {constructor (@union term (@union term R1 R2) (@union _ R3 (Pi pi V0 V1))) f} + {defined (@union term (@union term R1 R2) (@union _ R3 (Pi pi V0 V1))) f}.
proof: Proof. intros f; generalize (F.Symb.eq_bool_ok f pi); case (F.Symb.eq_bool f pi); [intros f_eq_pi | intros f_diff_pi]. subst; right. refine (Def _ pi (Var V0 :: Var V1 :: nil) (Var V0) _). do 2 right; apply Pi1. destruct (def_dec1 f) as [D1f | C1f]. right; inversion D1f as [f' k t H1]; subst f'. refine (Def _ f k t _); do 2 left; trivial. destruct (def_dec2 f) as [D2f | C2f]. right; inversion D2f as [f' k t H1]; subst f'. refine (Def _ f k t _); do 1 left; right; trivial. destruct (def_dec3 f) as [D3f | C3f]. right; inversion D3f as [f' k t H1]; subst f'. refine (Def _ f k t _); right; left; trivial. left; assert (Cf : forall k t, ~ (@union _ (@union _ R1 R2) (@union _ R3 (Pi pi V0 V1))) t (Term f k)). intros k t [[H1 | H2] | [H3 | HPi]]. apply C1f; apply (Def _ _ _ _ H1). apply C2f; apply (Def _ _ _ _ H2). apply C3f; apply (Def _ _ _ _ H3). inversion HPi; subst; absurd (f=f); trivial. apply Const; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)