proposition: Theorem Noetherian_contains_Noetherian : forall (U : Type) (R R' : Relation U), Noetherian R -> Contains R R' -> Noetherian R'.
proof: Proof. unfold Noetherian at 2 in |- *. intros U R R' H' H'0 x. elim H' with x; auto. Qed.
imports: Relations