some renaming and a minor addition

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
index 7489da1888424a5f4aca1e60754b06a0bf04b4f3..27c775019442a684aee2e46ad8c430a96c589ece 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
@@ -13,12 +13,12 @@
 (**************************************************************************)
 
 (* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES
- * Suggested invocation to start formal specifications with:
- *   - Patience on me to gain peace and perfection! -
+ * Initial invocation: - Patience on me to gain peace and perfection! -
  *)
 
-include "ground_2/star.ma".
-include "basic_2/notation.ma".
+include "ground_2/lib/star.ma".
+include "basic_2/notation/constructors/item0_0.ma".
+include "basic_2/notation/constructors/snitem2_2.ma".
 
 (* ATOMIC ARITY *************************************************************)
 
@@ -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,14 +48,14 @@ 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-.
 
 (* Basic properties *********************************************************)
 
-lemma aarity_eq_dec: ∀A1,A2:aarity. Decidable (A1 = A2).
+lemma eq_aarity_dec: ∀A1,A2:aarity. Decidable (A1 = A2).
 #A1 elim A1 -A1
 [ #A2 elim A2 -A2 /2 width=1/
   #B2 #A2 #_ #_ @or_intror #H destruct