freescle porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 0cdc02a4c5c2be7f36ef93e53beae6ea207f437b..2bf08ce485d0e7853e19889e316112df5dc3ba08 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -57,15 +57,6 @@ nlemma prop_to_nnprop : ∀P.P → ¬¬P.
  napply (H1 H).
 nqed.
 
-(*
-naxiom RAA : ∀P:Prop.∀f:(¬P) → False.P.
-
-nlemma nnprop_to_prop : ∀P.(¬¬P) → P.
- #P; nchange with (((¬P) → False) → P);
- #H; napply (RAA P H).
-nqed.
-*)
-
 ninductive And (A,B:Prop) : Prop ≝
  conj : A → B → (And A B).
 
@@ -94,32 +85,6 @@ interpretation "logical or" 'or x y = (Or x y).
 
 ndefinition decidable : Prop → Prop ≝ λA:Prop.A ∨ ¬A.
 
-(*
-nlemma decidable_prop : ∀P:Prop.decidable P.
- #P; nnormalize;
- napply RAA;
- #H;
- napply (absurd (P ∨ (¬P)) …);
- ##[ ##2: napply H
- ##| ##1: napply (or_intror P (¬P));
-          napply RAA;
-          #H1;
-          napply (absurd (P ∨ (¬P)) …);
-          ##[ ##2: napply H
-          ##| ##1: napply (or_introl P (¬P));
-                   napply (nnprop_to_prop P H1)
-          ##]
- ##]
-nqed.
-
-nlemma terzo_escluso : ∀P,G:Prop.∀ft:P → G.∀ff:(¬P) → G.G.
- #P; #G; nnormalize;
- #H; #H1;
- napply (Or_ind P (P → False) ? H H1 ?);
- napply (decidable_prop P).
-nqed.
-*)
-
 nlemma or_elim : ∀P,Q,G:Prop.Or P Q → ∀fp:P → G.∀fq:Q → G.G.
  #P; #Q; #G; #H; #H1; #H2;
  napply (Or_ind P Q ? H1 H2 ?);
@@ -191,21 +156,6 @@ nlemma neqf_to_neq : ∀T1,T2:Type.∀x,y:T1.∀f:T1 → T2.((f x) ≠ (f y)) 
  napply (H (eq_f … H1)).
 nqed.
 
-(*
-nlemma neqf2_to_neq : ∀T1,T2,T3:Type.∀x1,y1:T1.∀x2,y2:T2.∀f:T1 → T2 → T3.f x1 x2 ≠ f y1 y2 → (x1 ≠ y1) ∨ (x2 ≠ y2).
- #T1; #T2; #T3; #x1; #y1; #x2; #y2; #f; nnormalize; #H;
- napply (terzo_escluso (x1 = y1) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (terzo_escluso (x2 = y2) …)
-          ##[ ##2: #H2; napply (or_intror … H2)
-          ##| ##1: #H2; nrewrite < H1 in H:(%);
-                   nrewrite < H2; #H;
-                   nelim (H (refl_eq …))
-          ##]
- ##]
-nqed.
-*)
-
 nlemma symmetric_eq: ∀A:Type. symmetric A (eq A).
  #A;
  nnormalize;