- predefined_virtuals: some additions

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

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 eb3576d842c3689f43ea661b6ec17be7923a61ec..6d6993de3f137b561d551be5533c83d182ead802 100644 (file)
--- 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   : â\88\80V,T.           trf (â\93£V. T)
+| trf_cast   : â\88\80V,T.           trf (â\93\9dV. T)
 | trf_beta   : ∀V,W,T. trf (ⓐV. ⓛW. T)
 .