X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fsteps%2Frtc_shift.ma;h=a2746366cc458cf0f925767862f12d510a507fa1;hb=c3904c007394068ed823575e3be3d73a9ad92cce;hp=6cb0a8b1a43c524ef5be0ee210d3fcc90b8e6068;hpb=fb246e36bb7d2731016e686e2091f6a3704bb362;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
index 6cb0a8b1a..a2746366c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma
@@ -22,3 +22,9 @@ definition shift (r:rtc): rtc ≝ match r with
 
 interpretation "shift (rtc)"
    'Drop r = (shift r).
+
+(* Basic properties *********************************************************)
+
+lemma shift_refl: ∀ri,ti. 〈ri, 0, ti, 0〉 = ↓〈ri, 0, ti, 0〉.
+normalize //
+qed.