proposition: Lemma t_rt_step x y : r⁺ x y <-> (exists z, r＊ x z /\ r z y).
proof: Proof. split; ins; desf. by apply clos_trans_t1n in H; induction H; desf; eauto using clos_refl_trans. by rewrite clos_refl_transE in *; desf; eauto using clos_trans. Qed.
imports: HahnBase HahnList Relations