proposition: Lemma R2_var' : forall (v : variable) (t :term), ~ (@union _ R2 (Pi pi V0 V1)) t (Var v).
proof: Proof. intros v u [H2 | HPi]. 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)