proposition: Lemma cc_arg' E v V i (i1 : i < n) (i2 : i < arity (typ f)) : v = Vnth ls i1 -> V = Vnth (inputs (typ f)) i2 -> cc E v V.
proof: Proof. intros hv hV. subst. apply cc_arg. Qed.
imports: Coq(Morphisms Basics) CoLoR(LogicUtil LCompSimple VecUtil RelUtil LCall LCompInt SetUtil SN NatUtil LCompRewrite EqUtil)