X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Freduction%2Fcnr.ma;h=94045fca2c4a08e6d1ffcdb181cacf0c46f1fa64;hp=f1cdcf6316d12bd025feb4fb1239136e31bba256;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr.ma b/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr.ma
index f1cdcf631..94045fca2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr.ma
@@ -97,14 +97,14 @@ qed.
 lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}W.T⦄.
 #a #G #L #W #T #HW #HT #X #H
 elim (cpr_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
->(HW … HW0) -W0 >(HT … HT0) -T0 //
+<(HW … HW0) -W0 <(HT … HT0) -T0 //
 qed.
 
 (* Basic_1: was only: nf2_appl_lref *)
 lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄.
 #G #L #V #T #HV #HT #HS #X #H
 elim (cpr_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
->(HV … HV0) -V0 >(HT … HT0) -T0 //
+<(HV … HV0) -V0 <(HT … HT0) -T0 //
 qed.
 
 (* Basic_1: was: nf2_dec *)