proposition: Lemma G'_cp_red : cp_red (G' I_lt_a X).
proof: Proof. intros t u tu [ht1 ht2]. split. eapply SN_inv. apply tu. hyp. intros f hf ts hu. assert (ht : t =>R* apps (Fun f) ts). trans u. apply at_step. hyp. hyp. apply ht2; hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)