X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Faarity.ma;h=27c775019442a684aee2e46ad8c430a96c589ece;hb=fca909e9e53de73771e1b47e94434ae8f747d7fb;hp=88486384afb716cddf022da7937e99b1951dfa1e;hpb=50001ac0b45a3f6376e8cbfd9200149a01d68148;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
index 88486384a..27c775019 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
@@ -27,10 +27,10 @@ inductive aarity: Type[0] ≝
   | APair: aarity → aarity → aarity (* binary aarity construction *)
 .
 
-interpretation "aarity construction (atomic)"
+interpretation "atomic arity construction (atomic)"
    'Item0 = AAtom.
 
-interpretation "aarity construction (binary)"
+interpretation "atomic arity construction (binary)"
    'SnItem2 A1 A2 = (APair A1 A2).
 
 (* Basic inversion lemmas ***************************************************)
@@ -39,7 +39,7 @@ lemma discr_apair_xy_x: ∀A,B. ②B. A = B → ⊥.
 #A #B elim B -B
 [ #H destruct
 | #Y #X #IHY #_ #H destruct
-  -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
+  -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destructed equality is not erased *)
   /2 width=1/
 ]
 qed-.
@@ -48,7 +48,7 @@ lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → ⊥.
 #B #A elim A -A
 [ #H destruct
 | #Y #X #_ #IHX #H destruct
-  -H (**) (* destruct: the destucted equality is not erased *)
+  -H (**) (* destruct: the destructed equality is not erased *)
   /2 width=1/
 ]
 qed-.