proposition: Lemma acyclic_case_split A (r : relation A) f : acyclic r <-> acyclic (restr_rel f r) /\ (forall x (NEG: ~ f x) (CYC: r⁺ x x), False).
proof: Proof. unfold restr_rel; repeat split; repeat red; ins; desc; eauto. by eapply H, clos_trans_mon; eauto; instantiate; ins; desf. destruct (classic (f x)) as [K|K]; eauto. assert (M: (fun a b => r a b /\ f a /\ f b) ＊ x x) by vauto. generalize K; revert H0 M K; generalize x at 2 3 5; ins. apply clos_trans_tn1 in H0; induction H0; eauto 6 using rt_t_trans, t_step. destruct (classic (f y)); eauto 6 using clos_refl_trans. eapply H1; eauto. eapply t_rt_trans, rt_trans; eauto using t_step, clos_trans_in_rt, clos_tn1_trans. by eapply clos_refl_trans_mon; eauto; instantiate; ins; desf. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets