proposition: Lemma _dest_char_inj (a a' : ascii) : _dest_char a = _dest_char a' -> a = a'.
proof: Proof. induction a. induction a'. simpl. rewrite (@CONSTR_INJ (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop (prod Prop Prop)))))))). intros [e1[ e2 e3]]. assert (b = b7 /\ b0 = b8 /\ b1 = b9 /\ b2 = b10 /\ b3 = b11 /\ b4 = b12 /\ b5 = b13 /\ b6 = b14). apply pair_equal_spec in e2. repeat (rewrite pair_equal_spec in e2; split). apply eq_true_inj; apply e2. apply eq_true_inj; apply e2. apply eq_true_inj; apply e2. apply eq_true_inj; apply e2. apply eq_true_inj; apply e2. apply eq_true_inj; apply e2. split. apply eq_true_inj; apply e2. apply eq_true_inj; apply e2. destruct H; rewrite H. destruct H0; rewrite H0. destruct H1; rewrite H1. destruct H2; rewrite H2. destruct H3; rewrite H3. destruct H4; rewrite H4. destruct H5; rewrite H5. rewrite H6. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii