X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fllor_alt.ma;h=700cd7ce3ba9658d019b516f83ef37889c8898af;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=dd27e6a056170631627faa3725fe32de1aabc399;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma
index dd27e6a05..700cd7ce3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llor_alt.ma
@@ -36,8 +36,8 @@ elim (le_to_or_lt_eq … H) -H #H
   lapply (drop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
   elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
   [ /3 width=1 by and3_intro, or3_intro0/
-  | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/
-  | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/
+  | /7 width=2 by frees_inv_append, yle_inj, lt_to_le, or3_intro1, and3_intro/
+  | /6 width=1 by frees_append, yle_inj, lt_to_le, or3_intro2, and4_intro/
   ]
 | -IH -HLK1 destruct
   lapply (drop_O1_inv_append1_le … HLK2 … (⋆) ?) // -HLK2 normalize #H destruct
@@ -63,8 +63,8 @@ elim (le_to_or_lt_eq … H) -H #H
   lapply (drop_O1_inv_append1_le … HLK … HLY) /2 width=1 by lt_to_le/ -HLK normalize #H destruct
   elim (IH … HLY1 HLY2 HLY) -IH -HLY1 -HLY2 -HLY *
   [ /3 width=1 by and3_intro, or3_intro0/
-  | /6 width=2 by frees_inv_append, lt_to_le, or3_intro1, and3_intro/
-  | /5 width=1 by frees_append, lt_to_le, or3_intro2, and4_intro/
+  | /7 width=2 by frees_inv_append, yle_inj, lt_to_le, or3_intro1, and3_intro/
+  | /6 width=1 by frees_append, yle_inj, lt_to_le, or3_intro2, and4_intro/
   ]
 | -IH -HLK2 destruct
   lapply (drop_O1_inv_append1_le … HLK1 … (⋆) ?) // -HLK1 normalize #H destruct