- 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;
+ elim t1 using eq_ast_type_elim 0;
+ [ 1: intros 2;
+ elim t2 using eq_ast_type_elim 0;
+ [ 1: intros;
+ simplify in H;
+ rewrite > (eqastbasetype_to_eq ?? H);
+ reflexivity
+ | 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: simplify;
+ intros;
+ lapply (andb_true_true ?? H2) as H3;
+ lapply (andb_true_true_r ?? H2) as H4;
+ rewrite > (H ? H3);
+ rewrite > (eqb_true_to_eq ?? H4);
+ 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 in H2;
+ rewrite > (H x1);
+ [ reflexivity
+ | apply H2
+ ]
+ | 4: intros;
+ simplify in H3;
+ 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 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
+ ]