proposition: Lemma cc_acc' E v V g (us : TypArgs g) i (hi : Acc g i) : cc E (apps (Fun g) us) (Base (output_base (typ g))) -> v = Vnth us (Acc_arity hi) -> V = Vnth (inputs (typ g)) (Acc_arity hi) -> cc E v V.
proof: Proof. intros h hv hV. subst. apply cc_acc. hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)