-| rtm_ldelta: ∀G,u,E,t,F,V,S.
- rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0))
- (mk_rtm G u F S V)
-| rtm_ltype : ∀G,u,E,t,F,V,S.
- rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0))
- (mk_rtm G u F S V)
+| rtm_ldelta: ∀G,u,E,t,D,V,S.
+ rtm_step (mk_rtm G u (E. ④{Abbr} {t, D, V}) S (#0))
+ (mk_rtm G u D S V)
+| rtm_ltype : ∀G,u,E,t,D,V,S.
+ rtm_step (mk_rtm G u (E. ④{Abst} {t, D, V}) S (#0))
+ (mk_rtm G u D S V)