proposition: Lemma calls_sn : forall r s, (forall x, In x (vars r) -> SNR (s x)) -> (forall g vs, In (Fun g vs) (calls R r) -> Vforall SNR (Vmap (sub s) vs) -> SNR (sub s (Fun g vs))) -> forall a, In a (calls R r) -> SNR (sub s a).
proof: Proof. intros. ded (in_calls H1). destruct H2 as [g]. destruct H2 as [vs]. destruct H2. subst a. apply H0. hyp. eapply calls_sn_args. apply H. apply H0. hyp. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)