proposition: Lemma cc_call' E v V g p (us : Tes p) : 0+p <= arity (typ g) -> gt1 E (mk_call f ls) (mk_call g us) -> (forall i (i1 : i < p) (i2 : i < arity (typ g)), cc E (Vnth us i1) (Vnth (inputs (typ g)) i2)) -> v = apps (Fun g) us -> V = output (typ g) p -> cc E v V.
proof: Proof. intros h1 h2 h3 hv hV. subst. apply cc_call; hyp. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)