proposition: Lemma axiom_17 : forall (a : ascii), (_mk_char (_dest_char a)) = a.
proof: Proof. intro a. unfold _mk_char. match goal with [|- ε ?x = _] => set (A' := x); set (a' := ε A') end. assert (i : exists a', A' a'). exists a. reflexivity. generalize (ε_spec i). fold a'. unfold A', _mk_char_pred. apply _dest_char_inj. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii