proposition: Lemma append_single_char : forall s1 s2 a1 a2, append s1 (String a1 EmptyString) = append s2 (String a2 EmptyString) -> s1 = s2 /\ a1 = a2.
proof: Proof. induction s1; simpl. - destruct s2; simpl; intros; try discriminate. injection H; intros; subst; intuition. destruct s2; discriminate. - destruct s2; simpl; intros; try discriminate. injection H; intros; subst; intuition. destruct s1; discriminate. destruct s1; discriminate. injection H; intros; subst; intuition. apply IHs1 in H0; intuition subst; eauto. apply IHs1 in H0; intuition subst; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Numbers.Natural.Peano.NPeano Coq.Strings.String Coq.Arith.Lt Coq.Arith.Compare_dec Coq.Lists.List Coq.ZArith.ZArith