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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
index c34238632..49d6cf5b8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
@@ -40,7 +40,17 @@ interpretation "abstraction (local environment)"
 
 (* Basic properties *********************************************************)
 
-axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+lemma eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] * [2,4: #L2 #I2 #V2 ]
+[1,4: @or_intror #H destruct
+| elim (eq_bind2_dec I1 I2) #HI
+  [ elim (eq_term_dec V1 V2) #HV
+    [ elim (IHL1 L2) -IHL1 /2 width=1 by or_introl/ #HL ]
+  ]
+  @or_intror #H destruct /2 width=1 by/
+| /2 width=1 by or_introl/
+]
+qed-.
 
 (* Basic inversion lemmas ***************************************************)