proposition: Lemma is_char_of_string str ch : is_true (is_char (of_string str) ch) <-> str = (ch::nil).
proof: Proof. split; intro H; [ pose proof (length_singleton _ _ H) as H'; rewrite of_string_length in H' | ]; (destruct str as [|ch' [|ch'' str]]; simpl in *; try discriminate); change (ch' :: nil) with (List.take 1 (ch'::nil)) in *; repeat match goal with | [ H : _ |- _ ] => progress rewrite <- ?take_of_string, ?get_of_string in H | _ => progress rewrite <- ?take_of_string, ?get_of_string | _ => progress simpl in * | [ H : is_true (is_char _ _) |- _ ] => apply get_0 in H | [ |- is_true (is_char _ _) ] => apply get_0 | _ => progress unfold value in * | [ H : Some _ = Some _ |- _ ] => inversion_clear H | [ H : _::_ = _::_ |- _ ] => inversion_clear H | _ => reflexivity end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.Le Fiat.Common.Tactics.SetoidSubst Fiat.Common.Tactics.IsClosed Fiat.Parsers.StringLike.Core Fiat.Common.UIP