X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Fpar_reduction.ma;h=d906160ca53e1d65fc26387583ca89f45858933d;hb=9956360248d4d6cda67fb1363de22097ccaed533;hp=260157d4c28986faf5e28d750c60e6b38432ffc3;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy_new/par_reduction.ma b/matita/matita/lib/pts_dummy_new/par_reduction.ma
index 260157d4c..d906160ca 100644
--- a/matita/matita/lib/pts_dummy_new/par_reduction.ma
+++ b/matita/matita/lib/pts_dummy_new/par_reduction.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/subterms.ma".
+include "pts_dummy_new/subterms.ma".
 
 (*
 inductive T : Type[0] ≝
@@ -88,7 +88,7 @@ lemma prD: ∀M,N,P. pr (D M N) P →
    @(ex_intro … M2) @(ex_intro … N2) /3/
   ]
 qed.
-
+(* BEGIN HERE
 lemma prApp_not_lambda: 
 ∀M,N,P. pr (App M N) P → is_lambda M = false →
   ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
@@ -292,4 +292,4 @@ theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
 pr Q S ∧ pr P S.
 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 qed.
-
+*)