proposition: Lemma WF_chain : WF chain -> WF (red R).
proof: Proof. intro Hwf. unfold WF. apply term_ind_forall. apply sn_var. apply hyp1. intro f. case_eq (defined f R); intros. apply chain_fun. hyp. apply Hwf. hyp. apply sn_args_sn_fun; auto. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)