proposition: Lemma G'_cp_aeq : cp_aeq (G' I_lt_a X).
proof: Proof. intros t u tu [ht1 ht2]. split. rewrite <- tu. hyp. intros f hf ts. rewrite <- tu. fo. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)