fact: Definition good_ctx A (P: relation A -> relation A) := << MON: Morphisms.Proper (inclusion ==> inclusion) P >> /\ << CUN: forall (rr : nat -> relation A), P (⋃ n, rr n) ⊆ ⋃ n, P (rr n) >>.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets