[ 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'.
(* strlen *)
definition strLen_str ≝ λstr:aux_str_type.len_list ? str.
+
+(* ************ *)
+(* STRINGA + ID *)
+(* ************ *)
+
+(* tipo pubblico *)
+inductive aux_strId_type : Type ≝
+ STR_ID: aux_str_type → nat → aux_strId_type.
+
+(* getter *)
+definition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
+definition get_id_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID _ d ⇒ d ].
+
+(* confronto *)
+definition strCmp_strId ≝
+λsid,sid':aux_strId_type.(strCmp_str (get_name_strId sid) (get_name_strId sid'))⊗(eqb (get_id_strId sid) (get_id_strId sid')).