proposition: Lemma ct_imm1 : forall A (r : relation A) (I: irreflexive r) (T: transitive r) acts (FIN : dom_rel r ⊆₁ (fun x => In x acts)), r ≡ (immediate r)⁺.
proof: Proof. split; cycle 1. by rewrite immediateE, inclusion_minus_rel; auto with hahn. assert (M: forall x y, r x y -> In x (undup acts)). by ins; eapply in_undup_iff, FIN; vauto. red; ins; eapply clos_trans_imm; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets