proposition: Lemma F_ext : F I_lt_a [=] F J_lt_a.
proof: Proof. unfold F. apply lfp_ext. fo. fo. fo. intro X. apply G'_ext. refl. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)