Let $A = \{ 0, 1 \}$, the inductive type with two constant generators. One can prove (by induction) that the natural ordering on $A$ is well-founded in the sense of ($\ast$). Suppose it were well-founded in the sense of (${\ast}{\ast}$) instead. Let $Q$ be an arbitrary proposition and let $P$ be defined by induction as follows:
\begin{align}
P(0) & \equiv Q \\
P(1) & \equiv \top
\end{align}
Thus, there must exist $x_0 : A$ such that $P (x_0)$ and $\forall y : A . P (y) \to \lnot (y < x_0)$. But $\forall a : A . (a = 0) \lor (a = 1)$, so either $x_0 = 0$ or $x_0 = 1$. If $x_0 = 1$ then $P (0)$ holds, i.e. $Q$ holds. If $x_0 = 1$, then $P (0) \to \lnot (0 < 1)$, so $\lnot P (0)$ holds, i.e. $\lnot Q$ holds. Therefore $Q \lor \lnot Q$.
For those who like this kind of thing, here is a proof in Coq:
Inductive Two : Set :=
| zero : Two
| one : Two.
Definition LT (a : Two) (b : Two) : Prop.
destruct a.
destruct b.
exact False.
exact True.
exact False.
Defined.
Lemma LT_is_wf (P : Two -> Prop) (P_is_inductive : forall a : Two, (forall b : Two, (LT b a) -> P b) -> P a) : forall c : Two, P c.
Proof.
assert (P zero).
apply P_is_inductive.
intro b.
intro.
exfalso.
destruct b.
exact H.
exact H.
intro c.
destruct c.
exact H.
apply P_is_inductive.
intro b.
destruct b.
intro.
exact H.
intro.
exfalso.
exact H0.
Qed.
Lemma Two_is_decidable (a : Two) : (a = zero) \/ (a = one).
Proof.
destruct a.
auto.
auto.
Qed.
Definition decider (Q : Prop) : Two -> Prop.
intro a.
destruct a.
exact Q.
exact True.
Defined.
Theorem classical_wf_implies_lem (classical_wf : forall P : Two -> Prop, (exists a : Two, P a) -> (exists m : Two, P m /\ forall b : Two, P b -> not (LT b m))) (Q : Prop) : Q \/ not Q.
Proof.
set (P := decider Q).
assert (exists a : Two, P a).
exists one.
unfold P.
unfold decider.
tauto.
set (S := classical_wf P H).
destruct S.
destruct H0.
assert (x = zero -> Q).
intro.
cut (P zero).
tauto.
rewrite <- H2.
exact H0.
assert (x = one -> not Q).
intro.
intro.
refine (H1 zero _ _).
tauto.
rewrite H3.
unfold LT.
tauto.
cut (x = zero \/ x = one).
intro.
destruct H4.
left.
auto.
right.
auto.
exact (Two_is_decidable x).
Qed.