X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Freduction%2Fcnr_cir.ma;h=a6a90214dcf71c84627855378722354438f34672;hp=786611f54f1d3ddb482007c7546dff908b7c4514;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355 diff --git a/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr_cir.ma index 786611f54..a6a90214d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr_cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/reduction/cnr_cir.ma @@ -20,7 +20,7 @@ include "basic_2A/reduction/cnr_crr.ma". (* Main properties on irreducibility ****************************************) theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄. -/2 width=4 by cpr_fwd_cir/ qed. +/3 width=4 by cpr_fwd_cir, sym_eq/ qed. (* Main inversion lemmas on irreducibility **********************************)