proposition: Lemma I_eq_F : forall a, I a [=] F (I' a).
proof: Proof. intro a. unfold I. rewrite Fix_eq. refl. apply F_ext. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)