AST to ASTFE completed up to a few computational (!!!) axioms.

[helm.git] / helm / software / matita / contribs / assembly / string / string.ma

diff --git a/helm/software/matita/contribs/assembly/string/string.ma b/helm/software/matita/contribs/assembly/string/string.ma
index 4c4862928ff9a9b829a5ea6d4efa5ed1357b2832..f60b8a804c46f3a7bb5d42de6de1ffd1db4355ac 100755 (executable)
--- a/helm/software/matita/contribs/assembly/string/string.ma
+++ b/helm/software/matita/contribs/assembly/string/string.ma
@@ -48,6 +48,8 @@ let rec strCmp_str (str,str':aux_str_type) ≝
     [ true ⇒ strCmp_str t t' | false ⇒ false ]
   ]].
 
+axiom eqbstrcmpstr_to_eq : ∀s,s'.strCmp_str s s' = true → s = s'.
+
 (* strcat *)
 definition strCat_str ≝
 λstr,str':aux_str_type.str@str'.