Theorem markov_generalized (t : Inhabited) (p : t -> prp) :
  (forall x, trivial_C (p x)) ->
  (forall x, trivial_W (p x)) ->
  valid (neg (all x : t, neg (p x)) ==>> some x : t, p x).
Proof.
rewrite /valid /= => TC TW.
pose u := fun (h : _ -> {x : t & W (p x)}) =>
            let y := projT1 (h (fun x (_ : W (p x)) => C_member (p x))) in
            existT (fun x : t => W (p x)) y (W_member (p y)).
exists (u, fun _ x _ => C_member (p x))=>/=.
move=>[f g] /=.
pose v := projT1 (f (fun x _ => C_member (p x))).
pose w := projT2 (f (fun (x : t) (_ : W (p x)) => C_member (p x))).
rewrite (TC v (g v (W_member (p v)))) /=.
move: (TW v w); rewrite /w =>->/=.
by apply: dia_not_not_stable.
Qed.

Lemma dia_not_not_stable (p : prp) (w : W p) (c : C p) : ~ ~ dia w c -> dia w c.
Proof.
by move/classicP=>H; apply/diaP/H => /diaP.
Qed.