proposition: Lemma I_cp : (forall f n (ts : Tes n), ~neutral (apps (Fun f) ts)) -> forall a, cp (I a).
proof: Proof. intros hn a. induction (ltB_wf a) as [a _ IH]. rewrite I_eq_G'. constructor. apply G'_cp_aeq. apply G'_cp_sn. apply G'_cp_red. apply G'_cp_neutral. hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)