proposition: Lemma wf_restr r (WF: well_founded r) cond : well_founded (restr_rel cond r).
proof: Proof. red; ins; induction a using (well_founded_induction WF). constructor; ins; unfolder in H0; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom