proposition: Lemma module132' : module (@union term R1 R3) (@union term R2 (Pi pi V0 V1)).
proof: Proof. inversion module_R1_R3 as [M3]. inversion module_R1_R2 as [M2]. apply Mod. intros f s t Df [H1 | H3]. inversion Df as [f' l u [H2 | HPi]]; subst. apply M2; trivial; apply (Def R2 f l u); trivial. inversion HPi; subst f; subst. destruct (P1 s t H1 pi) as [Hs Ht]. simpl; destruct (symb_in_term pi s). absurd (pi = pi); trivial; apply Hs; trivial. destruct (symb_in_term pi t). absurd (pi = pi); trivial; apply Ht; trivial. trivial. destruct (P1 s t H1 pi) as [Hs Ht]. simpl; destruct (symb_in_term pi s). absurd (pi = pi); trivial; apply Hs; trivial. destruct (symb_in_term pi t). absurd (pi = pi); trivial; apply Ht; trivial. trivial. inversion Df as [f' l u [H2 | HPi]]; subst. apply Indep2; trivial; apply (Def R2 f l u); trivial. inversion HPi; subst f; subst. destruct (P3 s t H3 pi) as [Hs Ht]. simpl; destruct (symb_in_term pi s). absurd (pi = pi); trivial; apply Hs; trivial. destruct (symb_in_term pi t). absurd (pi = pi); trivial; apply Ht; trivial. trivial. destruct (P3 s t H3 pi) as [Hs Ht]. simpl; destruct (symb_in_term pi s). absurd (pi = pi); trivial; apply Hs; trivial. destruct (symb_in_term pi t). absurd (pi = pi); trivial; apply Ht; trivial. trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)