fixed or-in-left

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index b7ee07cb6da8135c294a57e32a1c9275826383c4..8a7399167dbad84a2cf4a8002e14aed19e035597 100644 (file)
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -285,7 +285,7 @@ interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab =
   (show ab (Or_intro_l _ _ a)).
 
 notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 
-for @{ 'Or_intro_l_ok_1 $a $ab }.
+for @{ 'Or_intro_l_ok_2 $a $ab }.
 interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = 
   (cast _ _ (show ab (Or_intro_l _ _ a))).