proposition: Lemma comp_acc : forall f (ts : Tes (arity (typ f))), I (output_base (typ f)) (apps (Fun f) ts) -> forall i (hi : Acc f i), int I (Vnth (inputs (typ f)) (Acc_arity hi)) (Vnth ts (Acc_arity hi)).
proof: Proof. intros f ts. set (a := output_base (typ f)). gen (I_eq a); unfold equiv, pointwise_relation; intro e; rewrite e; clear e. intros [h1 h2] i hi. apply h2; refl. Qed.
imports: Coq(IndefiniteDescription Structures.OrderedType) CoLoR(LogicUtil SN LCompSimple Tarski VecUtil SetUtil RelUtil)