proposition: Lemma chain_fun : forall f, defined f R = true -> forall ts, SN chain (Fun f ts) -> Vforall SNR ts -> SNR (Fun f ts).
proof: Proof. intros f defined_f ts sn_chain_f_ts sn_ts. apply chain_min_fun; auto. apply (SN_incl chain). apply chain_min_incl_chain. hyp. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)