proposition: Lemma char_eq : char_pred = char_ind.
proof: Proof. apply fun_ext. intro r. apply prop_ext. intro h. apply h. intros r' H. destruct H as [a0 [a1 [a2 [a3 [a4 [a5 [a6 [a7 e]]]]]]]]. rewrite e. rewrite (Prop_bool_eq a0). rewrite (Prop_bool_eq a1). rewrite (Prop_bool_eq a2). rewrite (Prop_bool_eq a3). rewrite (Prop_bool_eq a4). rewrite (Prop_bool_eq a5). rewrite (Prop_bool_eq a6). rewrite (Prop_bool_eq a7). exact (char_ind_cons (@COND bool a0 true false) (@COND bool a1 true false) (@COND bool a2 true false) (@COND bool a3 true false) (@COND bool a4 true false) (@COND bool a5 true false) (@COND bool a6 true false) (@COND bool a7 true false)). induction 1. unfold char_pred. intros R h. apply h. exists a0. exists a1. exists a2. exists a3. exists a4. exists a5. exists a6. exists a7. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii