- nat.ma: we added a general induction principle

[helm.git] / matita / matita / contribs / lambda / term.ma

diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma
index 2e6a6e0ec16eaf566cf0a5ef3012837560a8d58d..8c688dc8e9b10f874836791a38f5edfc36e64878 100644 (file)
--- a/matita/matita/contribs/lambda/term.ma
+++ b/matita/matita/contribs/lambda/term.ma
@@ -44,10 +44,6 @@ notation "hvbox( 𝛌  . term 46 A )"
    non associative with precedence 46
    for @{ 'Abstraction $A }.
 
-notation > "hvbox( 𝛌 term 46 A )"
-   non associative with precedence 46
-   for @{ 'Abstraction $A }.
-
 notation "hvbox( @ term 46 C . break term 46 A )"
    non associative with precedence 46
    for @{ 'Application $C $A }.