X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fterms%2Fsequential_reduction.ma;h=becaaac787b3ffeecb7a6174696465c885b395dd;hb=249addcfcf2681df796236b0f39a71260dddaa79;hp=cfd1fbe7f56aebb43eac5c003b2c0a6a3b8426fd;hpb=5c792a695677f2857e1984ababc9998d42fc8033;p=helm.git

diff --git a/matita/matita/contribs/lambda/terms/sequential_reduction.ma b/matita/matita/contribs/lambda/terms/sequential_reduction.ma
index cfd1fbe7f..becaaac78 100644
--- a/matita/matita/contribs/lambda/terms/sequential_reduction.ma
+++ b/matita/matita/contribs/lambda/terms/sequential_reduction.ma
@@ -42,7 +42,7 @@ qed-.
 lemma sred_inv_abst: ∀M,N. M ↦ N → ∀C1. 𝛌.C1 = M →
                      ∃∃C2. C1 ↦ C2 & 𝛌.C2 = N.
 #M #N * -M -N
-[ #B #A #C #H destruct
+[ #B #A #C1 #H destruct
 | #A1 #A2 #HA12 #C1 #H destruct /2 width=3/
 | #B1 #B2 #A #_ #C1 #H destruct
 | #B #A1 #A2 #_ #C1 #H destruct