milestone update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma
index 414fa1bfe62428cb1e00a7268b4f16313eab87e3..6d75613c6838ea7abaaae97547aacba4268f487e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma
@@ -17,7 +17,7 @@ include "ground/notation/functions/tuple_4.ma".
 include "ground/notation/functions/zerozero_0.ma".
 include "ground/notation/functions/zeroone_0.ma".
 include "ground/notation/functions/onezero_0.ma".
-include "ground/insert_eq/insert_eq_1.ma".
+include "ground/generated/insert_eq_1.ma".
 include "ground/arith/nat.ma".
 
 (* RT-TRANSITION COUNTERS ***************************************************)
@@ -34,19 +34,19 @@ record rtc: Type[0] ≝ {
 }.
 
 interpretation
-  "constructor (rtc)"
+  "construction (rt-transition counters)"
   'Tuple ri rs ti ts = (mk_rtc ri rs ti ts).
 
 interpretation
-  "one structural step (rtc)"
+  "one structural step (rt-transition counters)"
   'ZeroZero = (mk_rtc nzero nzero nzero nzero).
 
 interpretation
-  "one r-step (rtc)"
+  "one r-step (rt-transition counters)"
   'OneZero = (mk_rtc nzero (ninj punit) nzero nzero).
 
 interpretation
-  "one t-step (rtc)"
+  "one t-step (rt-transition counters)"
   'ZeroOne = (mk_rtc nzero nzero nzero (ninj punit)).
 
 definition rtc_eq_f: relation rtc ≝ λc1,c2. ⊤.
@@ -58,7 +58,8 @@ inductive rtc_eq_t: relation rtc ≝
 
 (* Basic constructions ******************************************************)
 
-lemma rtc_eq_t_refl: reflexive …  rtc_eq_t.
+lemma rtc_eq_t_refl:
+      reflexive …  rtc_eq_t.
 * // qed.
 
 (* Basic inversions *********************************************************)