Library Computability

Lemma dec_pdec P : ldec P → ∀ x, P x ∨ ¬ P x.

Definition cChoice := constructive_indefinite_ground_description_nat_Acc.

Lemma eq_term_dec (s t : term) : (s = t) + (s ≠ t).

Lemma enc_inj m n : enc m == enc n → m = n.

Lemma dec_dec P u : (∀ s, u (tenc s) == true ∧ P s ∨ u (tenc s) == false ∧ ¬ P s) → ∀ s, dec(P s).