proposition: Lemma good_ctx_compose P (GP : good_ctx P) Q (GQ : good_ctx Q) : good_ctx (fun x => P (Q x)).
proof: Proof. cdes GP; cdes GQ; split; unnw; ins; [by do 2 red; ins; rewrite H|]. rewrite CUN0, CUN; apply inclusion_bunion_l; vauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets