proposition: Lemma clos_trans_restr_trans_cycle : forall X (r r' : relation X) f x y (A : clos_trans (restr_rel f (r ∪ r')) x y) (B : r y x), clos_trans (restr_rel f (r ∪ r')) x x.
proof: Proof. ins; eapply t_trans, t_step; unfold union; eauto. red; apply clos_trans_restrD in A; desf; auto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath