fact: Fixpoint afs_filt (l : list M.term) (ns : list nat) : list M.term := match ns with | n::ns => match nth_error l n with | Some t => t :: afs_filt l ns | _ => afs_filt l ns end | _ => nil end.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)