]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/ground/steps/rtc_isrt.ma
update in bin
[helm.git] / matita / matita / contribs / lambdadelta / ground / steps / rtc_isrt.ma
index 7f9f2f74ad1d7e891662dcf7d0dd2abfeb9cacd1..66717209694982a291a1b5888c87fccf98667f99 100644 (file)
@@ -20,7 +20,7 @@ include "ground/steps/rtc.ma".
 definition isrt: relation2 nat rtc ≝ λts,c.
                  ∃∃ri,rs. 〈ri,rs,0,ts〉 = c.
 
-interpretation "test for costrained rt-transition counter (rtc)"
+interpretation "test for constrained rt-transition counter (rtc)"
    'IsRedType ts c = (isrt ts c).
 
 (* Basic properties *********************************************************)