milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpt_drops.ma

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 1d4e8b33a5b5c479101be1a29e470969eab67e7e..29cbdfc0d7f7e903160d721e1feb37753abc5df2 100644 (file)
--- 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/