update in ground

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / models / tm_props.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
index 1f3c49413751079a74cb8f929037afa1e43f7c5e..1777a2d000a874f4f603ac57a1484b0082a726ae 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma
@@ -38,7 +38,7 @@ lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T):
 
 
 <pippo in ⊢ (????%?); >(mf_comp … T) in ⊢ (????%?);
-[2: @@tm_vpush_vlift_join_O
+[2: ;;tm_vpush_vlift_join_O
 
 <pippo in ⊢ (????%?);