update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / counters / rtc_ist.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma
index 57ba73e327d5bcf0e32cfe75b4c1a72605de3064..525745120e54bbf26793ef1425f10b03c0398900 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc_ist.ma
@@ -26,32 +26,32 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma rtc_ist_zz: ð\9d\90\93â\9dªð\9d\9f\8e,ð\9d\9f\98ð\9d\9f\98â\9d«.
+lemma rtc_ist_zz: ð\9d\90\93â\9d¨ð\9d\9f\8e,ð\9d\9f\98ð\9d\9f\98â\9d©.
 // qed.
 
-lemma rtc_ist_zu: ð\9d\90\93â\9dªð\9d\9f\8f,ð\9d\9f\98ð\9d\9f\99â\9d«.
+lemma rtc_ist_zu: ð\9d\90\93â\9d¨ð\9d\9f\8f,ð\9d\9f\98ð\9d\9f\99â\9d©.
 // qed.
 
 (* Basic inversions *********************************************************)
 
-lemma rtc_ist_inv_zz (n): ð\9d\90\93â\9dªn,ð\9d\9f\98ð\9d\9f\98â\9d« → 𝟎 = n.
+lemma rtc_ist_inv_zz (n): ð\9d\90\93â\9d¨n,ð\9d\9f\98ð\9d\9f\98â\9d© → 𝟎 = n.
 #n #H destruct //
 qed-.
 
-lemma rtc_ist_inv_zu (n): ð\9d\90\93â\9dªn,ð\9d\9f\98ð\9d\9f\99â\9d« → ninj (𝟏) = n.
+lemma rtc_ist_inv_zu (n): ð\9d\90\93â\9d¨n,ð\9d\9f\98ð\9d\9f\99â\9d© → ninj (𝟏) = n.
 #n #H destruct //
 qed-.
 
-lemma rtc_ist_inv_uz (n): ð\9d\90\93â\9dªn,ð\9d\9f\99ð\9d\9f\98â\9d« → ⊥.
+lemma rtc_ist_inv_uz (n): ð\9d\90\93â\9d¨n,ð\9d\9f\99ð\9d\9f\98â\9d© → ⊥.
 #h #H destruct
 qed-.
 
 (* Main inversions **********************************************************)
 
-theorem rtc_ist_inj (n1) (n2) (c): ð\9d\90\93â\9dªn1,câ\9d« â\86\92 ð\9d\90\93â\9dªn2,câ\9d« → n1 = n2.
+theorem rtc_ist_inj (n1) (n2) (c): ð\9d\90\93â\9d¨n1,câ\9d© â\86\92 ð\9d\90\93â\9d¨n2,câ\9d© → n1 = n2.
 #n1 #n2 #c #H1 #H2 destruct //
 qed-.
 
-theorem rtc_ist_mono (n) (c1) (c2): ð\9d\90\93â\9dªn,c1â\9d« â\86\92 ð\9d\90\93â\9dªn,c2â\9d« → c1 = c2.
+theorem rtc_ist_mono (n) (c1) (c2): ð\9d\90\93â\9d¨n,c1â\9d© â\86\92 ð\9d\90\93â\9d¨n,c2â\9d© → c1 = c2.
 #n #c1 #c2 #H1 #H2 destruct //
 qed-.