proposition: Lemma I_eq : forall a, I a [=] G a I.
proof: Proof. intro a. rewrite I_eq_G'. unfold G'. apply G_ext. intros b h. unfold update. destruct (BOrd.compare b a). refl. rewrite e. refl. fo. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)