proposition: Lemma rest_union : forall A P (R1 R2 : relation A) a b, rest P (union _ R1 R2) a b <-> union _ (rest P R1) (rest P R2) a b.
proof: Proof. intros A P R1 R2 a b; split. intros [[H1 | H2] [Pa Pb]]; [left | right]; repeat split; assumption. intros [[H1 [Pa Pb]] | [H2 [Pa Pb]]]; repeat split; trivial. left; assumption. right; assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)