proposition: Lemma union_idem_strong : forall A (R R': A -> A -> Prop) (H:forall x y, R x y -> R' x y) x y, (union A R R' x y <-> R' x y).
proof: Proof. intros A R R' H x y. split. inversion_clear 1. apply H;assumption. assumption. intro H';right;assumption. Qed.
imports: Coq(Setoid Relations List Wellfounded)