proposition: Lemma eqb_spec s1 s2 : Bool.reflect (s1 = s2) (s1 =? s2)%string.
proof: Proof. revert s2. induction s1 as [|? s1 IHs1]; intro s2; destruct s2; try (constructor; easy); simpl. case Ascii.eqb_spec; simpl; [intros -> | constructor; now intros [= ]]. case IHs1; [intros ->; now constructor | constructor; now intros [= ]]. Qed.
imports: Arith Ascii Bool Coq.Strings.Byte