xoa: change in naming convenctions for existential quantifies

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / grammar / term_weight.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
index d8f39a3a154de4d7c53ca040220ef80ee4a118e2..3f9fbef8775b55a2e353acea9aafbedceca23a44 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
@@ -30,14 +30,8 @@ lemma tw_pos: ∀T. 1 ≤ #{T}.
 #T elim T -T //
 qed.
 
-(* Basic eliminators ********************************************************)
-
-axiom tw_ind: ∀R:predicate term.
-              (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) →
-              ∀T. R T.
-
 (* Basic_1: removed theorems 11:
             wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
             weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
-            removed local theorems 1: q_ind
 *)
+(* Basic_1: removed local theorems 1: q_ind *)