proposition: Lemma map_rel_ct f r : (f ↓ r)⁺ ⊆ f ↓ r⁺.
proof: Proof. u. induction H. { apply ct_step. eauto. } apply ct_ct. eexists. eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets