[ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
].
+lemma eqastbasetype_to_eq : ∀t1,t2:ast_base_type.(eq_ast_base_type t1 t2 = true) → (t1 = t2).
+ unfold eq_ast_base_type;
+ intros;
+ elim t1 in H:(%);
+ elim t2 in H:(%);
+ normalize in H:(%);
+ try reflexivity;
+ destruct H.
+qed.
+
let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
match t1 with
[ AST_TYPE_BASE bType1 ⇒ match t2 with
| _ ⇒ false ]
].
+lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
+ intro;
+ elim t1 0; [1,3:intros 2 | intros 4] elim t2;
+ [ 2,5,7,9: normalize in H1; destruct H1;
+ | 3,4: normalize in H; destruct H;
+ | 1: simplify in H;
+ apply (eq_f ?? (λx.? x) a a1 (eqastbasetype_to_eq a a1 H))
+ | 8: simplify in H2;
+ lapply (andb_true_true ? ? H2);
+ lapply (andb_true_true_r ? ? H2); clear H2;
+ rewrite > (H ? Hletin);
+ rewrite > (eqb_true_to_eq ?? Hletin1);
+ reflexivity
+ | 6: elim daemon;
+ ].
+qed.
+
definition is_ast_base_type ≝
λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].