freescale porting, work in progress

[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 82a33c9f8d4bbcb2a00aa2148ebf843266af7af1..c04bc9df094b61ec224db740d5d9fbcbd9e83188 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
@@ -56,8 +56,8 @@ nlemma symmetric_eqoption :
  (symmetricT T bool f) →
  (eq_option T op1 op2 f = eq_option T op2 op1 f).
  #T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
  nnormalize;
  ##[ ##1: napply (refl_eq ??)
  ##| ##2,3: #H; napply (refl_eq ??)
@@ -72,8 +72,8 @@ nlemma eq_to_eqoption :
  (∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
  (op1 = op2 → eq_option T op1 op2 f = true).
  #T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply (refl_eq ??)
  ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
@@ -90,8 +90,8 @@ nlemma eqoption_to_eq :
  (∀x1,x2:T.f x1 x2 = true → x1 = x2) →
  (eq_option T op1 op2 f = true → op1 = op2).
  #T; #op1; #op2; #f; #H;
- napply (option_ind T ??? op1);
- napply (option_ind T ??? op2);
+ nelim op1;
+ nelim op2;
  nnormalize;
  ##[ ##1: #H1; napply (refl_eq ??)
  ##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)