- predefined_virtuals: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / tnf.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
index 294546af97d8bd8da1822ea74cffb6b4bdcb5480..2e357a292d1523cc025b60d2ad75422d4b5a81c7 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma
@@ -53,7 +53,7 @@ lemma tnf_inv_abbr: ∀V,T. 𝐍⦃ⓓV.T⦄ → ⊥.
 ]
 qed.
 
-lemma tnf_inv_cast: â\88\80V,T. ð\9d\90\8dâ¦\83â\93£V.T⦄ → ⊥.
+lemma tnf_inv_cast: â\88\80V,T. ð\9d\90\8dâ¦\83â\93\9dV.T⦄ → ⊥.
 #V #T #H lapply (H T ?) -H /2 width=1/ #H
 @discr_tpair_xy_y //
 qed-.