proposition: Lemma acyclic_restr A d (r: relation A) : acyclic r -> acyclic (restr_rel d r).
proof: Proof. eauto using acyclic_mon with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath