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