freescle porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
index c157bfa11a64af79534fe638c8dbeda604ebc8ed..34d63c6016d4f9fd66229c44a35af5c5b60339c0 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma
@@ -99,36 +99,3 @@ nlemma eqoption_to_eq :
           napply refl_eq
  ##]
 nqed.
-
-nlemma neq_to_neqoption :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
- (∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
- (op1 ≠ op2 → eq_option T op1 op2 f = false).
- #T; #op1; #op2; #f; #H;
- nelim op1;
- nelim op2;
- nnormalize;
- ##[ ##1: #H1; napply False_ind; napply (H1 (refl_eq …))
- ##| ##2,3: #a; #H1; napply refl_eq
- ##| ##4: #a; #a0; #H1;
-          napply H;
-          napply (neqf_to_neq … a0 a (λx.Some ? x) H1)
- ##]
-nqed.
-
-nlemma neqoption_to_neq :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
- (∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
- (eq_option T op1 op2 f = false → op1 ≠ op2).
- #T; #op1; #op2; #f; #H;
- nelim op1;
- nelim op2;
- nnormalize;
- ##[ ##1: #H1; napply (bool_destruct … H1)
- ##| ##2: #a; #H1; #H2; napply (option_destruct_none_some ? a H2)
- ##| ##3: #a; #H1; #H2; napply (option_destruct_some_none ? a H2)
- ##| ##4: #a; #a0; #H1; #H2;
-          napply (H a0 a H1);
-          napply (option_destruct_some_some ? a0 a H2)
- ##]
-nqed.