proposition: Lemma union_assoc : forall A R1 R2 R3 x y, union A (union A R1 R2) R3 x y <-> union A R1 (union A R2 R3) x y.
proof: Proof. intros A R1 R2 R3 x y. split. intro H. case H;clear H;intro H. case H;clear H;intro H. left;assumption. right;left;assumption. right;right;assumption. intro H. case H;clear H;intro H. left;left;assumption. case H;clear H;intro H. left;right;assumption. right;assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)