λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / jsx_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma
index 7ac21a90d5d142b1254813193005e9bf2e38b567..74eb68212c40253d3b039426a4bd7ac60f29d7f3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/jsx_drops.ma
@@ -47,7 +47,7 @@ elim (drops_inv_bind1_isuni … H) -H [3,6: // |*: * -Hf ]
 [1,3: #Hf #H destruct -IH /3 width=3 by drops_refl, ex2_intro/
 |2,4:
   #g #Hg #HK1 #H destruct
-  elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2 
+  elim (IH … Hg … HK1) -K1 -Hg #Y2 #HY12 #HKY2
   /3 width=3 by drops_drop, ex2_intro/
 ]
 qed-.