proposition: Lemma string_append_nil : forall s1 s2, append s1 s2 = "" -> s1 = "" /\ s2 = "".
proof: Proof. induction s1; simpl; eauto. intros; discriminate. 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