milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / reduction / cnr_cir.ma

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 786611f54f1d3ddb482007c7546dff908b7c4514..a6a90214dcf71c84627855378722354438f34672 100644 (file)
--- 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 **********************************)