fact: Fixpoint map12_without_repetition (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (f : A -> option B * option B) (l : list A) {struct l} : list B := match l with | nil => (nil : list B) | h :: nil => match f h with | (None, None) => nil | (Some f_h1, None) => f_h1 :: nil | (None, Some f_h1) => f_h1 :: nil | (Some f_h1, Some f_h2) => f_h1 :: f_h2 :: nil end | h :: ((h' :: tl) as l1) => if (eqA h h') then map12_without_repetition eqA f l1 else match f h with | (None, None) => map12_without_repetition eqA f l1 | (Some f_h1, None) => f_h1 :: (map12_without_repetition eqA f l1) | (None, Some f_h1) => f_h1 :: (map12_without_repetition eqA f l1) | (Some f_h1, Some f_h2) => f_h2 :: f_h1 :: (map12_without_repetition eqA f l1) end end.
imports: List Arith