proposition: Lemma sn_args_sn_fun : forall f, defined f R = false -> forall ts, Vforall SNR ts -> SNR (Fun f ts).
proof: Proof. intros. set (gt := @Vrel1 (arity f) _ Red). assert (SN gt ts). unfold gt. apply Vforall_SN_rel1. hyp. elim H1. intros. apply SN_intro. change (forall y, Red (Fun f x) y -> SNR y). intros. redtac. subst y. destruct c; simpl in xl; simpl. case (fun_eq_sub xl); intro H4; destruct H4. cut (defined f R = true). rewrite H. discr. eapply lhs_fun_defined. subst l. apply lr. subst l. is_var_lhs. Funeqtac. subst x. apply H3. unfold gt. eapply Vrel1_cast_intro. apply Vrel1_app_intro_l. apply Vrel1_cons_intro. left. split. 2: refl. apply red_rule. hyp. Qed.
imports: CoLoR(ATrs SN LogicUtil VecUtil VecOrd NatUtil RelUtil ARelation Union ACap ACalls) Coq(List Sumbool)