proposition: Lemma clos_trans_imm : forall A (r : relation A) (I: irreflexive r) (T: transitive r) L (ND: NoDup L) a b (D: forall c, r a c -> r c b -> In c L) (REL: r a b), (immediate r)⁺ a b.
proof: Proof. intros until 3; induction ND; ins; vauto. destruct (classic (r a x /\ r x b)) as [|N]; desf; [apply t_trans with x|]; eapply IHND; ins; forward (by eapply (D c); eauto) as K; desf; exfalso; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets