- one axiom removed from sd

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / grammar / lenv_weight.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
index d277ed00eafb8647a8ff8c9e31653f58d48674d6..59e2e6172bc24a83e79d60cdb537e2e403087cae 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
@@ -31,9 +31,9 @@ lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
 
 (* Basic eliminators ********************************************************)
 
-axiom lw_wf_ind: ∀R:predicate lenv.
-                 (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
-                 ∀L. R L.
+axiom lw_ind: ∀R:predicate lenv.
+              (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
+              ∀L. R L.
 
 (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
 (* Basic_1: note: clt_thead should be renamed clt_ctail *)