- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / apps_2 / functional / rtm_step.ma

diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
index bf04f72c9e53828ba58f849a747252fc9ce2c57f..ed16d509193deffb3cf4f64f108b311f0c527b1b 100644 (file)
--- a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
+++ b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma
@@ -43,13 +43,13 @@ inductive rtm_step: relation rtm ≝
               rtm_step (mk_rtm G u E S (ⓐV. T))
                        (mk_rtm G u E ({E, V} @ S) T)
 | rtm_beta  : ∀G,u,E,F,V,S,W,T.
-              rtm_step (mk_rtm G u E ({F, V} @ S) (ⓛW. T))
+              rtm_step (mk_rtm G u E ({F, V} @ S) (+ⓛW. T))
                        (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
 | rtm_push  : ∀G,u,E,W,T.
-              rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
+              rtm_step (mk_rtm G u E ⟠ (+ⓛW. T))
                        (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T)
 | rtm_theta : ∀G,u,E,S,V,T.
-              rtm_step (mk_rtm G u E S (ⓓV. T))
+              rtm_step (mk_rtm G u E S (+ⓓV. T))
                        (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
 .