proposition: Lemma G'_cp_neutral : (forall f n (ts : Tes n), ~neutral (apps (Fun f) ts)) -> cp_neutral (G' I_lt_a X).
proof: Proof. intros hn t ht1 ht2. split. apply SN_intro. intros u tu. destruct (ht2 _ tu) as [h _]. hyp. intros f hf ts r. destruct (clos_aeq_trans_inv _ r) as [h|[u [h1 h2]]]. rewrite h in ht1. fo. eapply ht2. apply h1. hyp. hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)