- revision of ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lcosx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
index 8997c6ec9b567531a19bae6ec23b32d0e817aa23..b19af406733a5c781c399140ce2f7a980b1cde46 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx.ma
@@ -58,7 +58,7 @@ fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ~⬊*[h, g, x] L → ∀l. x = ⫯l
                                   G ⊢ ⬊*[h, g, V, l] K.
 #h #g #G #L #l * -L -l /2 width=1 by or_introl/
 [ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H)
-| #I #L #T #l #HT #HL #x #H <(ysucc_inj … H) -x
+| #I #L #T #l #HT #HL #x #H <(ysucc_inv_inj … H) -x
   /3 width=6 by ex3_3_intro, or_intror/
 ]
 qed-.