proposition: Lemma Incomp123' : forall f, defined (@union _ R1 R2) f -> defined (@union _ R3 (Pi pi V0 V1)) f -> False.
proof: Proof. intros f D12f D3f'; inversion D12f as [f' l u [H1 | H2]]; clear D12f; subst; inversion D3f' as [f'' l' u' [H3 | Hpi]]; clear D3f'; subst. apply (Incomp13 f (Def R1 f l u H1) (Def R3 f l' u' H3)). inversion Hpi; subst f; apply (Incomp1' (Def R1 pi l u H1)). apply (Incomp23 f (Def R2 f l u H2) (Def R3 f l' u' H3)). inversion Hpi; subst f; apply (Incomp2' (Def R2 pi l u H2)). Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)