proposition: Lemma dom_helper A dom (s: relation A) (IN: s ⊆ ⦗fun x => In x dom⦘ ⨾ s ⨾ ⦗fun x => In x dom⦘) a (INa: In a dom) b (H: s ＊ a b) : In b dom.
proof: Proof. ins; apply clos_refl_transE in H; desf. apply t_rt_step in H; desc. apply IN in H0; revert H0; basic_solver. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn