...

diff --git a/helm/software/matita/contribs/assembly/compiler/ast_type.ma b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
index 8ad0220ffa804cc0db0823a12593a35efbd7e39a..b1ad547e9485e4d189df2e3cc3828d9cc6f9f870 100755 (executable)
--- a/helm/software/matita/contribs/assembly/compiler/ast_type.ma
+++ b/helm/software/matita/contribs/assembly/compiler/ast_type.ma
@@ -76,42 +76,22 @@ let rec eq_ast_type (t1,t2:ast_type) on t1 ≝
   ].
 
 lemma eqasttype_to_eq : ∀t1,t2:ast_type.(eq_ast_type t1 t2 = true) → (t1 = t2).
- do 2 intro;
- cases t1; cases t2;
- [ 2,3,4,6,7,8: normalize; intro; destruct H
- | 1: change in ⊢ (? ? % ?→?) with (eq_ast_base_type a a1);
-      intro;
+ 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))
- | 5: change in ⊢ (? ? % ?→?) with ((eq_ast_type a a1) ⊗ (eqb n n1));
-      intro;
-      cut (a = a1 ∧ n = n1);
-      elim daemon.
- | 9: elim daemon
+ | 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.
 
-(* PERCHE' ??
- se in testa includo
- include "demo/natural_deduction.ma".
- la dimostrazione va fino in fondo ma poi impazzisce ast_tree.ma
- dicendo che la dichiarazione ast_id e' scorretta
- 
-      [ 1: alias id "And_elim_l" = "cic:/matita/demo/natural_deduction/And_elim_l.con".
-           alias id "And_elim_r" = "cic:/matita/demo/natural_deduction/And_elim_r.con".
-           apply (eq_f2 ??? (λx.λy.? x y) a a1 n n1 (And_elim_l ?? Hcut) (And_elim_r ?? Hcut))
-      | 2: split;
-           [ 2: apply (eqb_true_to_eq n n1 (andb_true_true_r ?? H))
-           | 1: cut (eq_ast_Type a a1 = true);
-                [ 2: apply (andb_true_true ?? H)
-                | 1: TODO elim daemon
-                ]
-           ]
-      ]
- | 9: TODO elim daemon
- ]
-qed.
-*)
-
 definition is_ast_base_type ≝
 λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].