proposition: Lemma calls_sn_args : 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 g vs, In (Fun g vs) (calls R r) -> Vforall SNR (Vmap (sub s) vs).
proof: Proof. intros r s H H0. cut (forall a g vs, a = Fun g vs -> In a (calls R r) -> Vforall SNR (Vmap (sub s) vs)). intros. apply H1 with (a := Fun g vs). refl. hyp. intro a. pattern a. apply subterm_ind. clear a. intros. subst t. apply Vforall_intro. intros w H2. ded (Vin_map H2). destruct H4 as [v]. destruct H4. subst w. assert (v = sub (alien_sub R v) (cap R v)). apply sym_eq. apply (alien_sub_cap R). rewrite H5, sub_sub. apply no_call_sub_sn. apply calls_cap. intros. assert (subterm v r). eapply subterm_trans_eq2 with (u := Fun g vs). apply subterm_fun. hyp. eapply in_calls_subterm. apply H3. unfold sub_comp. unfold alien_sub. case (le_lt_dec x (maxvar v)); intro. rewrite fsub_inf. 2: hyp. simpl. apply H. eapply subterm_eq_vars. apply subterm_strict. apply H7. apply (vars_cap_inf R). hyp. hyp. ded (vars_cap R H6). rewrite (fsub_nth (aliens (capa R v)) l H8). set (a := Vnth (aliens (capa R v)) (lt_pm (k:=projT1 (capa R v)) l H8)). assert (Vin a (aliens (capa R v))). unfold a. apply Vnth_in. assert (subterm_eq a v). apply (in_aliens_subterm R). hyp. assert (In a (calls R v)). apply aliens_incl_calls. hyp. ded (in_calls H11). destruct H12 as [f]. destruct H12 as [us]. destruct H12. rewrite H12. rewrite H12 in H10. rewrite H12 in H11. assert (In (Fun f us) (calls R r)). apply subterm_in_calls. hyp. apply subterm_strict. eapply subterm_trans_eq1. apply H10. hyp. apply H0. hyp. apply H1 with (u := Fun f us). eapply subterm_trans_eq1. eapply in_calls_subterm. apply H11. apply subterm_fun. hyp. refl. hyp. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)