fact: Fixpoint afs_term (afs_symb : M.symbol -> afs_val) (t : M.term) : M.term := match t with | M.Var _ => t | M.Term f l => let l' := map (afs_term afs_symb) l in match afs_symb f with | AFS_id f => M.Term f l' | AFS_arg n => nth n l' (M.Term f nil) | AFS_filt f ns => M.Term f (afs_filt l' ns) end end.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)