+ | 4: intros 5;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H2
+ | 2: simplify;
+ intros;
+ destruct H3
+ | 3: simplify;
+ intros;
+ destruct H3
+ | 4: intros;
+ simplify in H4;
+ lapply (andb_true_true ?? H4) as H5;
+ lapply (andb_true_true_r ?? H4) as H6;
+ rewrite > (H ? H5);
+ lapply depth=0 (H1 (AST_TYPE_STRUCT l1)) as K;
+ destruct (K ?);
+ [ apply H6
+ | reflexivity
+ ]
+ ]
+ ].
+qed.
+
+lemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type t1 t2 = true.
+ intro;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H;
+ apply (eq_to_eqastbasetype x x (refl_eq ??))
+ | 2: simplify;
+ intros;
+ destruct H1
+ | 3: simplify;
+ intros;
+ destruct H1
+ | 4: simplify;
+ intros;
+ destruct H2
+ ]
+ | 2: intros 4;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: intros;
+ simplify;
+ destruct H2;
+ rewrite > (H t (refl_eq ??));
+ rewrite > (eq_to_eqb_true n n (refl_eq ??));
+ reflexivity
+ | 3: simplify;
+ intros;
+ destruct H2
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 3: intros 3;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H1
+ | 2: simplify;
+ intros;
+ destruct H2
+ | 3: intros;
+ simplify;
+ destruct H2;
+ rewrite > (H x (refl_eq ??));
+ reflexivity
+ | 4: simplify;
+ intros;
+ destruct H3
+ ]
+ | 4: intros 5;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: simplify;
+ intros;
+ destruct H2
+ | 2: simplify;
+ intros;
+ destruct H3
+ | 3: simplify;
+ intros;
+ destruct H3
+ | 4: intros;
+ simplify;
+ destruct H4;
+ rewrite > (H x (refl_eq ??));
+ rewrite > (H1 (AST_TYPE_STRUCT l) (refl_eq ??));
+ reflexivity
+ ]
+ ].