proposition: Lemma R123_var' : forall v t, ~ (@union _ (@union _ R1 R2) (@union _ R3 (Pi pi V0 V1))) t (Var v).
proof: Proof. intros v t [[H1 | H2] | [H3 | HPi]]. apply (R1_var _ _ H1). apply (R2_var _ _ H2). apply (R3_var _ _ H3). inversion HPi. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)