(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / option_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
index 071d884f475accee1a91af1536f9eecc416c185f..30df5ac07ce6f277a3ed92ca745647b2f56bf4c3 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
@@ -57,7 +57,7 @@ nqed.
 
 nlemma bsymmetric_eqoption :
 ∀T:Type.∀o1,o2:option T.∀f:T → T → bool.
- (boolSymmetric T f) →
+ (symmetricT T bool f) →
  (eq_option T o1 o2 f = eq_option T o2 o1 f).
  #T; #o1; #o2; #f; #H;
  ncases o1;
@@ -95,7 +95,7 @@ nlemma eqoption_to_eq :
  ncases o1;
  ncases o2;
  ##[ ##1: nnormalize; #H1; napply (refl_eq ??)
- ##| ##2,3: #H1; #H2; nnormalize in H2:(%); nelim (bool_destruct_false_true H2)
+ ##| ##2,3: #H1; #H2; nnormalize in H2:(%); napply (bool_destruct ??? H2)
  ##| ##4: #x1; #x2; #H1;
           nnormalize in H1:(%);
           nrewrite > (H ?? H1);