fact: Fixpoint diffElem (L1 : list A) : list A -> option A := fun L2 : list A => match L1 with | nil => None | a :: L'1 => match InEqDec a L2 with | left _ => diffElem L'1 L2 | right _ => Some a end end.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)