X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fcounters%2Frtc.ma;h=6d75613c6838ea7abaaae97547aacba4268f487e;hb=2e4a7c54ef77c10cb1cef4b59518c473245ea935;hp=414fa1bfe62428cb1e00a7268b4f16313eab87e3;hpb=dbc57c92512c04b3fd88f8289bb8dbe99b2f90e0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma
index 414fa1bfe..6d75613c6 100644
--- 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 *********************************************************)