Library AD

Require Import Por Acceptability.

Theorem AD M : (forall x, M x \/ ~ M x) -> lacc M -> lacc (complement M) -> ldec M.
Proof.
  intros pdec_M [u [[cls_u lam_u] Hu]] [v [[cls_v lam_v] Hv]].
  pose (por_u_v := lam (Por ((App (tenc u) (Q #0))) ((App (tenc v) (Q #0))))).
  exists por_u_v.
  split; value. intros t.

  assert (A : converges (Por (tenc (u (tenc t))) (tenc (v (tenc t))))). {
    eapply Por_correct_1.
    destruct (pdec_M t); firstorder.
  }

  destruct (Por_correct_2 A) as [[B C] | [B C]].
  - left; split; try firstorder 2.
    transitivity (((Por ((App (tenc u) ( Q (tenc t))))) ((App (tenc v) (Q (tenc t)))))). unfold por_u_v. crush.
    now rewrite !Q_correct, !App_correct.
  - right; split; try firstorder 2.
    transitivity (((Por ((App (tenc u) ( Q (tenc t))))) ((App (tenc v) (Q (tenc t)))))). unfold por_u_v; crush.
    now rewrite !Q_correct, !App_correct.
Qed.