1) PTS simplified

[helm.git] / helm / software / matita / contribs / ng_assembly / utility / ascii_lemmas1.ma

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 4c371c1bebf10df099845b30231f0ab800083841..efab13f9dc46e62f566600069002f2f53488ea53 100755 (executable)
--- 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.