letin are no longer unfolded thus coercions not propagated deeply.

workaround not using letins

diff --git a/helm/software/matita/tests/coercions_russell.ma b/helm/software/matita/tests/coercions_russell.ma
index 203faece5d6db7e13ef284842fe397502e6a0bb3..c386743e74f466edcf5bff9938d9d9142b6de1de 100644 (file)
--- a/helm/software/matita/tests/coercions_russell.ma
+++ b/helm/software/matita/tests/coercions_russell.ma
@@ -44,13 +44,13 @@ qed.
 
 alias symbol "exists" (instance 3) = "exists".
 lemma tl2 : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l.
-letin program ≝ 
-  (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]);
-letin program_spec ≝ 
-  (program : ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l);
-  [ autobatch; | generalize in match H; clear H; cases s; simplify;
-    intros; cases (H H1); ]
-exact program_spec.
+apply
+  (λl:list nat. match l with [ nil ⇒ [] | cons x l1 ⇒ l1]
+  :
+  ∀l:∃l:list nat. l ≠ []. ∃l1.∃a.a :: l1 = l);
+[ autobatch; 
+| generalize in match H; clear H; cases s; simplify;
+  intros; cases (H H1);]
 qed.
 
 definition nat_return := λn:nat. Some ? n.
@@ -101,23 +101,19 @@ simplify; apply (eqb_elim x hd); simplify; intros;
 simplify; autobatch;
 qed.
 
-definition if : ∀A:Type.bool → A → A → A ≝ 
- λA,b,t,f. match b with [ true ⇒ t | false ⇒ f].
- 
-notation < "'If' \nbsp b \nbsp 'Then' \nbsp t \nbsp 'Else' \nbsp f" for @{ 'if $b $t $f }.
-notation > "'If' b 'Then' t 'Else' f" for @{ 'if $b $t $f }.
-interpretation "if" 'if a b c = (cic:/matita/tests/coercions_russell/if.con _ a b c). 
+notation > "'If' b 'Then' t 'Else' f" 
+for @{ match $b with [ true ⇒ $t | _ ⇒ $f ] }.
 
 definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res).
 (* define the find function *) 
-letin find ≝ (λp. 
+apply (λp. 
   let rec aux l ≝
     match l with
     [ nil ⇒ raise_exn
     | cons x l ⇒ If p x Then nat_return x Else aux l]
-    in aux);
-(* manca una delta?! *) unfold if in find;
-apply (find: ∀p.∀l.sigma ? (λres.find_spec l p res)); clear find;
+    in aux
+  : 
+  ∀p.∀l.sigma ? (λres.find_spec l p res));
 (* l = x::tl ∧ p x = false *)
 [1: cases (aux l1); clear aux;
     generalize in match H2; clear H2; cases a; clear a; simplify;