X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Fterm.ma;h=fc039863e108caa96c9def45f1052b16f87f1da1;hb=67c5cf7ae14c745a94defbe645c5406ccbcf514d;hp=77725446a9ebf79e1aedd380433dd4f315bc702d;hpb=0c7129d74ba0bfbdf7f71ffcf46a8c8c93e7df14;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
index 77725446a..fc039863e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
@@ -93,7 +93,18 @@ interpretation "native type annotation (term)"
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: term_dec *)
-axiom eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
+lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
+#T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ]
+[1,4: @or_intror #H destruct
+| elim (eq_item2_dec I1 I2) #HI
+  [ elim (IHV1 V2) -IHV1 #HV
+    [ elim (IHT1 T2) -IHT1 /2 width=1 by or_introl/ #HT ]
+  ]
+  @or_intror #H destruct /2 width=1 by/
+| elim (eq_item0_dec I1 I2) /2 width=1 by or_introl/ #HI
+  @or_intror #H destruct /2 width=1 by/
+]
+qed-.
 
 (* Basic inversion lemmas ***************************************************)