proposition: Lemma axiom_18' : forall (r : recspace (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop)))))))), char_pred r = ((_dest_char (_mk_char r)) = r).
proof: Proof. intro r. apply prop_ext. intro h. apply (@ε_spec _ (_mk_char_pred r)). rewrite char_eq in h. induction h. exists (Ascii a0 a1 a2 a3 a4 a5 a6 a7). reflexivity. intro e. rewrite <- e. intros P h. apply h. destruct (_mk_char r); simpl. exists (is_true b). exists (is_true b0). exists (is_true b1). exists (is_true b2). exists (is_true b3). exists (is_true b4). exists (is_true b5). exists (is_true b6). reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii