The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Aug 22, 2014 at 8:47 AM, John Wiegley 
<johnw AT newartisans.com>
 wrote:
> Yes, Xavier, with these hints I was able to solve it!  I still cannot find a
> way to solve it without using excluded_middle, however.  Do you have a hint 
> in
> that direction?

How about applying a lemma like:
forall x l1 l2 l3, (forall y, appears_in y l1 -> appears_in y (l2 ++ x
:: l3)) ->
appears_in x l1 \/ (forall y, appears_in y l1 -> appears_in y (l2 ++ l3)).

At least, that resolves where I was thinking of using EM in the proof
with Xavier's hint.
-- 
Daniel Schepler