- substitution lemma for native type assignmenr proved!

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / notation.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index e56344d7dd677a2a361c9739263b87705b187045..398ca7df43c1a35c1730af4ce50162f89bab14a8 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -316,19 +316,19 @@ notation "hvbox( ⬇ * term 46 T  )"
    non associative with precedence 45
    for @{ 'SN $T }.
 
-notation "hvbox( L ⊢ ⬇ * term 46 T )"
+notation "hvbox( L ⊢ break ⬇ * term 46 T )"
    non associative with precedence 45
    for @{ 'SN $L $T }.
 
-notation "hvbox( L ⊢ ⬇ ⬇ * term 46 T )"
+notation "hvbox( L ⊢ break ⬇ ⬇ * term 46 T )"
    non associative with precedence 45
    for @{ 'SNAlt $L $T }.
 
-notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )"
+notation "hvbox( ⦃ L, break T ⦄ ϵ break [ R ] break 〚 A 〛 )"
    non associative with precedence 45
    for @{ 'InEInt $R $L $T $A }.
 
-notation "hvbox( T1 break [ R ] ⊑ break term 46 T2 )"
+notation "hvbox( T1 ⊑ break [ R ] break term 46 T2 )"
    non associative with precedence 45
    for @{ 'CrSubEq $T1 $R $T2 }.