proposition: Lemma good_ctx_const r : good_ctx (fun x : relation A => r).
proof: Proof. split; unnw; ins; repeat red; ins; vauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets