- partial commit of rt_transition ...

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / steps / rtc_shift.ma

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 6cb0a8b1a43c524ef5be0ee210d3fcc90b8e6068..a2746366cc458cf0f925767862f12d510a507fa1 100644 (file)
--- 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.