proposition: Lemma G'_ext : forall X Y, X [=] Y -> G' I_lt_a X [=] G' J_lt_a Y.
proof: Proof. intros X Y XY t. unfold G'. apply G_ext. intro b. unfold update. destruct (BOrd.compare b a); fo. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)