- dynamic type assignment dismissed for now

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
index a745dd844cd48247ba4ca5a050b1942999e8b389..26e2d137b58f53e3b6d6842af9c98a8470162520 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma
@@ -35,7 +35,7 @@ generalize in match HVT; -HVT elim T -T //
 * // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
 qed-.
 
-lemma tif_inv_cast: â\88\80V,T. ð\9d\90\88â¦\83â\93£V.T⦄ → ⊥.
+lemma tif_inv_cast: â\88\80V,T. ð\9d\90\88â¦\83â\93\9dV.T⦄ → ⊥.
 /2 width=1/ qed-.
 
 (* Basic properties *********************************************************)