From 876b7e94113e67c7fb2dbc9ff7956c399778ce6f Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 8 Mar 2014 16:57:47 +0000
Subject: [PATCH] some corrections ...

---
 .../contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma    | 2 +-
 matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma    | 2 +-
 matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma     | 5 ++++-
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
index cdb3f2fbc..61466ca35 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma
@@ -23,7 +23,7 @@ include "basic_2/computation/lsx.ma".
 lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L.
 #h #g #G #L1 #d #i #HL1 @lsx_intro
 #L2 #HL12 #H elim H -H
-/4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux/
+/4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_conf_aux/
 qed.
 
 lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
index 6578c4cd9..f7f23760d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
@@ -174,7 +174,7 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L2| = |L1|.
+lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize //
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 555a340d8..92b07e1f2 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -52,7 +52,10 @@ lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
 
 (* Properties ***************************************************************)
 
-fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
+fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
 // qed-.
 
 lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
-- 
2.39.2