fact: Fixpoint getSomes(A : Type)(ls : list (option A)) := match ls with | nil => nil | o :: ls' => match o with | None => getSomes ls' | Some x => x :: (getSomes ls') end end.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation