fact: Fixpoint permute(ls : list A)(sigma : list nat) : list A := match sigma with | nil => nil | n :: sigma' => match (nth_error ls n) with | None => nil | Some a => a :: (permute ls sigma') end end.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation