X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftif.ma;h=26e2d137b58f53e3b6d6842af9c98a8470162520;hb=b074ebf6441993694c6e39e4eaeeb58a3186f479;hp=a745dd844cd48247ba4ca5a050b1942999e8b389;hpb=5ac2dc4e01aca542ddd13c02b304c646d8df9799;p=helm.git

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 a745dd844..26e2d137b 100644
--- 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: ∀V,T. 𝐈⦃ⓣV.T⦄ → ⊥.
+lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓝV.T⦄ → ⊥.
 /2 width=1/ qed-.
 
 (* Basic properties *********************************************************)