freescale 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 2ce5c7036deb6f45b405573846d9f53f48ff418e..31cb11c9ce0ccd06b0f587f8625f1b65a0e1441a 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -527,13 +527,14 @@ ndefinition associative : ∀A:Type.∀R:relationT A A.Prop ≝
 λA.λR.∀x,y,z:A.R (R x y) z = R x (R y z).
 
 (* aggiunta per bypassare i punti in cui le dimostrazioni sono equivalenti *)
-
+(*
 ninductive peqv (A:Prop) (x:A) : A → Prop ≝
  prefl_eqv : peqv A x x.
 
 interpretation "prop equivalence" 'preqv t x y = (peqv t x y).
-
+*)
 (* \equiv *)
+(*
 notation > "hvbox(a break ≡ b)" 
   non associative with precedence 45
 for @{ 'preqv ? $a $b }.
@@ -552,7 +553,7 @@ nlemma peqv_ind_r: ∀A:Prop.∀x:A.∀P:A → Prop.P x → ∀y:A.y ≡ x → P
 nqed.
 
 naxiom peqv_ax : ∀P:Prop.∀Q,R:P.Q ≡ R.
-
+*)
 (* uso P x → P y, H e' P x
    nrewrite > cioe' napply (peqv_ind ? x (λ_.?) H y (dimostrazione di x ≡ y));
    nrewrite < cioe' napply (peqv_ind_r ? x ? H y (dimostrazione y ≡ x)));