X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpt_drops.ma;h=29cbdfc0d7f7e903160d721e1feb37753abc5df2;hp=1d4e8b33a5b5c479101be1a29e470969eab67e7e;hb=3c7b4071a9ac096b02334c1d47468776b948e2de;hpb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma
index 1d4e8b33a..29cbdfc0d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_drops.ma
@@ -72,7 +72,7 @@ lemma cpt_inv_atom_sn_drops (h) (n) (I) (G) (L):
 #h #n #I #G #L #X2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
 [ #H1 #H2 destruct
   /3 width=1 by or4_intro0, conj/
-| #s #H1 #H2 #H3 destruct
+| #s1 #s2 #H1 #H2 #H3 #H4 destruct
   /3 width=3 by or4_intro1, ex3_intro/
 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
   /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/