proposition: Lemma fsupp_rt r (ACYC: acyclic r) s (DOMA: doma r s) (TOT: has_finite_antichains s r) : fsupp r -> fsupp r＊.
proof: Proof. eauto using fsupp_ct_rt, fsupp_ct. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom