proposition: Lemma immediate_clos_trans_elim A (r : relation A) a b : immediate (r⁺) a b -> r a b /\ (forall c, r⁺ a c -> r⁺ c b -> False).
proof: Proof. unfold immediate; ins; desf; split; ins. apply t_step_rt in H; desf. apply clos_refl_transE in H1; desf; exfalso; eauto using t_step. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets