proposition: Lemma union_equiv_list : forall R1 R1_list R2 R2_list (H1: forall l r, R1 r l <-> In (l,r) R1_list) (H2: forall l r, R2 r l <-> In (l,r) R2_list), forall l r, union term R1 R2 r l <-> In (l, r) (R1_list ++ R2_list).
proof: Proof. intros R1 R1_list R2 R2_list H1 H2 l r. split. intros [H|H];apply in_or_app;[rewrite <- H1|rewrite <- H2];auto with *. intros H;destruct (@in_app_or _ _ _ _ H) as [H' | H']; [left;rewrite H1|right;rewrite H2];auto with *. Qed.
imports: Coq(Relations List Setoid) CoLoR(weaved_relation closure equational_theory_spec dp modular_dp terminaison)