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