proposition: Lemma module123' : module (@union term R1 R2) (@union term R3 (Pi pi V0 V1)).
proof: Proof. inversion module_R1_R2 as [M2]. inversion module_R1_R3 as [M3]. apply Mod. intros f s t Df [H1 | H2]. inversion Df as [f' l u [H3 | HPi]]; subst. apply M3; trivial; apply (Def R3 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 [H3 | HPi]]; subst. apply Indep3; trivial; apply (Def R3 f l u); trivial. inversion HPi; subst f; subst. destruct (P2 s t H2 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 (P2 s t H2 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)