proposition: Lemma R132_reg' : forall s t, @union _ (@union _ R1 R3) (@union _ R2 (Pi pi V0 V1)) s t -> forall x, In x (var_list s) -> In x (var_list t) .
proof: Proof. intros s t [[H1 | H3] | [H2 | HPi]]. apply (R1_reg _ _ H1). apply (R3_reg _ _ H3). apply (R2_reg _ _ H2). inversion HPi as [ H1 | H2]. intros x [x_eq_v1 | x_in_nil]; [idtac | contradiction]. subst; left; trivial. intros x [x_eq_v1 | x_in_nil]; [idtac | contradiction]. subst; right; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)