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