(* Various small results used in at least two files in the front-end. *)

include "Clight/TypeComparison.ma".

lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
* normalize //
qed.

lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
* normalize // 
qed.

lemma type_eq_identity : ∀t. type_eq t t = true.
#t normalize elim (type_eq_dec t t)
[ 1: #Heq normalize //
| 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.

lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false.
#t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2)
[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
| 2: #Hneq' normalize // ] qed.