proposition: Lemma comp_fun : (forall f n (ts : Tes n), ~neutral (apps (Fun f) ts)) -> forall f (ts : Tes (arity (typ f))), vint I (inputs (typ f)) ts -> (forall u, apps (Fun f) ts =>R u -> I (output_base (typ f)) u) -> I (output_base (typ f)) (apps (Fun f) ts).
proof: Proof. intros hn f ts hts h. set (a := output_base (typ f)). gen (I_cp hn a). intros [a1 a2 a3 a4]. gen (I_eq a); unfold equiv, pointwise_relation; intro e; rewrite e; clear e. split. apply SN_intro. fo. intros g hg us r i hi. destruct (clos_aeq_trans_inv _ r) as [j|[v [h1 h2]]]. inv_aeq j; subst. gen (eq_apps_fun_head i0). intro e. subst g. apply eq_apps_nb_args_args in i0. subst us0. apply vint_elim_nth. eapply vint_vaeq. apply I_cp. hyp. sym. apply i2. hyp. gen (h _ h1). fold a. gen (I_eq a); unfold equiv, pointwise_relation; intro e; rewrite e; clear e. intros [i1 i2]. apply i2; hyp. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)