proposition: Lemma no_call_sub_sn : forall t, calls R t = nil -> forall s, (forall x, In x (vars t) -> SNR (s x)) -> SNR (sub s t).
proof: Proof. intro. pattern t. apply term_ind_forall; clear t; intros. ded (H0 v). apply H1. simpl. auto. rewrite sub_fun. pattern (defined f R). apply bool_eq_ind; intro. simpl in H0. rewrite H2 in H0. discr. apply sn_args_sn_fun. hyp. apply Vforall_map_intro. apply Vforall_intro. intros. ded (Vforall_in H H3). apply H4. simpl in H0. rewrite H2 in H0. change (vcalls R v = nil) in H0. eapply in_vcalls_nil with (n := arity f). apply H3. hyp. intros. apply H1. rewrite vars_fun. eapply vars_vec_in. apply H5. hyp. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)