proposition: Lemma WF_absorb : WF R -> WF (E# @ R).
proof: Proof. rewrite !WF_notIS_eq. intros wf f hf. destruct (IS_absorb hf) as [g hg]. fo. Qed.
imports: CoLoR(RelUtil NatUtil Path LeastNat LogicUtil ClassicUtil SN NotSN_IS SortUtil ListUtil) Coq(IndefiniteDescription)