X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Futility%2Fascii_lemmas1.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Futility%2Fascii_lemmas1.ma;h=efab13f9dc46e62f566600069002f2f53488ea53;hb=33b04453963755b619ac644f988e86a09cd54d63;hp=4c371c1bebf10df099845b30231f0ab800083841;hpb=63741bdebe93f58cef3ea791ca634ef17237bd7f;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
index 4c371c1be..efab13f9d 100755
--- a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
@@ -30,7 +30,7 @@ include "freescale/theory.ma".
 ndefinition ascii_destruct1 : Πc2.ΠP:Prop.ch_0 = c2 → match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ].
  #c2; #P; ncases c2; nnormalize;
  ##[ ##1: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  ##]
 nqed.