proposition: Lemma union_equiv : forall A R1 R2 R3 R4 (R1_equiv_R3: forall x y, R1 x y <-> R3 x y) (R2_equiv_R4: forall x y, R2 x y <-> R4 x y) x y, (union A R1 R2 x y <-> union _ R3 R4 x y).
proof: Proof. intros A R1 R2 R3 R4 R1_equiv_R3 R2_equiv_R4 x y. split;intro H;case H. rewrite R1_equiv_R3;intro H';left;exact H'. rewrite R2_equiv_R4;intro H';right;exact H'. rewrite <- R1_equiv_R3;intro H';left;exact H'. rewrite <- R2_equiv_R4;intro H';right;exact H'. Qed.
imports: Coq(Setoid Relations List Wellfounded)