+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.
+