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

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnx.ma
index e754c0a1f..4a03a7130 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnx.ma
@@ -33,7 +33,7 @@ lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄ → de
 lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_st/ -L -d #H
 lapply (destruct_tatom_tatom_aux … H) -H #H (**) (* destruct lemma needed *)
 lapply (destruct_sort_sort_aux … H) -H #H (**) (* destruct lemma needed *)
-lapply (next_lt h k) >H -H #H elim (lt_refl_false … H)
+lapply (next_lt h k) <H -H #H elim (lt_refl_false … H)
 qed-.
 
 lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄ → ⊥.
@@ -122,14 +122,14 @@ lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃W⦄ → ⦃G,
                 ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}W.T⦄.
 #h #g #a #G #L #W #T #HW #HT #X #H
 elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
->(HW … HW0) -W0 >(HT … HT0) -T0 //
+<(HW … HW0) -W0 <(HT … HT0) -T0 //
 qed.
 
 lemma cnx_appl_simple: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → 𝐒⦃T⦄ →
                        ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓐV.T⦄.
 #h #g #G #L #V #T #HV #HT #HS #X #H
 elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
->(HV … HV0) -V0 >(HT … HT0) -T0 //
+<(HV … HV0) -V0 <(HT … HT0) -T0 //
 qed.
 
 axiom cnx_dec: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T1⦄ ∨