X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftrf.ma;h=6d6993de3f137b561d551be5533c83d182ead802;hb=cb38da6095e3af84131a3ebf47a9f252f34a804c;hp=eb3576d842c3689f43ea661b6ec17be7923a61ec;hpb=db7ecce6c398a42f14557067bf18b61cf75da80e;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
index eb3576d84..6d6993de3 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma
@@ -23,7 +23,7 @@ inductive trf: predicate term ≝
 | trf_appl_sn: ∀V,T.   trf V → trf (ⓐV. T)
 | trf_appl_dx: ∀V,T.   trf T → trf (ⓐV. T)
 | trf_abbr   : ∀V,T.           trf (ⓓV. T)
-| trf_cast   : ∀V,T.           trf (ⓣV. T)
+| trf_cast   : ∀V,T.           trf (ⓝV. T)
 | trf_beta   : ∀V,W,T. trf (ⓐV. ⓛW. T)
 .