some corrections ...

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 cdb3f2fbc4bbd7ffce648484f0179dee0f8cb93c..61466ca351f3771d8c0ba8b57d033dd5ea14f74f 100644 (file)
--- 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 6578c4cd9235ea6cc1fe8c40b1a5f29475c392da..f7f23760d8594c36af97c4b1c5986cd343798b0d 100644 (file)
--- 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 555a340d880d582bc5f08fa6afbc151175a2e833..92b07e1f2b9525a4bbd743f498ede54a2860e057 100644 (file)
--- 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.