+(* confronto *)
+let rec eq_aux_env_type_aux (subE,subE':list var_elem) on subE ≝
+ match subE with
+ [ nil ⇒ match subE' with
+ [ nil ⇒ true | cons _ _ ⇒ false ]
+ | cons h tl ⇒ match subE' with
+ [ nil ⇒ false | cons h' tl' ⇒ (strCmp_str (get_name_var h) (get_name_var h'))⊗
+ (eq_bool (get_const_desc (get_desc_var h)) (get_const_desc (get_desc_var h')))⊗
+ (eq_ast_type (get_type_desc (get_desc_var h)) (get_type_desc (get_desc_var h')))⊗
+ (eq_aux_env_type_aux tl tl') ]
+ ].
+
+axiom eqbauxenvtypeaux_to_eq : ∀e,e'.eq_aux_env_type_aux e e' = true → e = e'.
+
+let rec eq_aux_env_type (e,e':aux_env_type) on e ≝
+ match e with
+ [ ne_nil h ⇒ match e' with
+ [ ne_nil h' ⇒ eq_aux_env_type_aux h h' | ne_cons _ _ ⇒ false ]
+ | ne_cons h tl ⇒ match e' with
+ [ ne_nil h' ⇒ false | ne_cons h' tl' ⇒ (eq_aux_env_type_aux h h')⊗(eq_aux_env_type tl tl') ]
+ ].
+
+axiom eqbauxenvtype_to_eq : ∀e,e':aux_env_type.eq_aux_env_type e e' = true → e = e'.
+