From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 13 Mar 2016 17:30:14 +0000 (+0000)
Subject: - new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
X-Git-Tag: make_still_working~631
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=5832735b721c0bd8567c8f0be761a9136363a2a6

- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)
- source specifier on inductive/coinductive types (implies matitaclan all)
- minor additions
---

diff --git a/matita/components/binaries/Makefile b/matita/components/binaries/Makefile
index 66af4a5f6..15ff284f3 100644
--- a/matita/components/binaries/Makefile
+++ b/matita/components/binaries/Makefile
@@ -2,8 +2,9 @@ H=@
 
 #CSC: saturate is broken after the huge refactoring of auto/paramodulation
 #CSC: by Andrea
-#BINARIES=extractor  table_creator  utilities saturate
-#BINARIES=transcript
+#BINARIES=extractor  table_creator  utilities saturate transcript
+#FG: my binaries
+BINARIES=mac matex matitadep probe xoa
 
 all: $(BINARIES:%=rec@all@%) 
 opt: $(BINARIES:%=rec@opt@%)
diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index baf92236c..49002d108 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -281,7 +281,7 @@ let string_of_source = function
    | `Generated -> "generated "
 
 let pp_obj pp_term = function
- | Ast.Inductive (params, types) ->
+ | Ast.Inductive (params, types, source) ->
     let pp_constructors constructors =
       String.concat "\n"
         (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
@@ -295,7 +295,8 @@ let pp_obj pp_term = function
     | [] -> assert false
     | (name, inductive, typ, constructors) :: tl ->
         let fst_typ_pp =
-          sprintf "%sinductive %s%s: %s \\def\n%s"
+          sprintf "%s%sinductive %s%s: %s \\def\n%s"
+            (string_of_source source)
             (if inductive then "" else "co") name (pp_params pp_term params)
             (pp_term typ) (pp_constructors constructors)
         in
@@ -309,7 +310,8 @@ let pp_obj pp_term = function
       (match body with
       | None -> ""
       | Some body -> "\\def\n " ^ pp_term body)
- | Ast.Record (params,name,ty,fields) ->
+ | Ast.Record (params,name,ty,fields, source) ->
+    string_of_source source ^
     "record " ^ name ^ " " ^ pp_params pp_term params ^ ": " ^ pp_term ty ^ 
     " \\def {" ^ pp_fields pp_term fields ^ "\n}"
  | Ast.LetRec (kind, definitions, (source, _, _)) ->
diff --git a/matita/components/content/notationPt.ml b/matita/components/content/notationPt.ml
index 52d433aa2..c718a20ba 100644
--- a/matita/components/content/notationPt.ml
+++ b/matita/components/content/notationPt.ml
@@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option
 
 (** To be increased each time the term type below changes, used for "safe"
  * marshalling *)
-let magic = 7
+let magic = 8
 
 type term =
   (* CIC AST *)
@@ -173,7 +173,7 @@ type cic_appl_pattern =
 type 'term inductive_type = string * bool * 'term * (string * 'term) list
 
 type 'term obj =
-  | Inductive of 'term capture_variable list * 'term inductive_type list
+  | Inductive of 'term capture_variable list * 'term inductive_type list * NCic.source
       (** parameters, list of loc * mutual inductive types *)
   | Theorem of string * 'term * 'term option * NCic.c_attr
       (** name, type, body, attributes
@@ -183,7 +183,7 @@ type 'term obj =
        *   will be given in proof editing mode using the tactical language,
        *   unless the flavour is an Axiom
        *)
-  | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
+  | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list * NCic.source
       (** left parameters, name, type, fields *)
   | LetRec of induction_kind * ('term capture_variable list * 'term capture_variable * 'term * int) list * NCic.f_attr
       (* (params, name, body, decreasing arg) list, attributes *)
diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index 823febdb6..82096f80b 100644
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -362,21 +362,21 @@ let freshen_obj obj =
   let freshen_capture_variable (n, t) = freshen_term n, HExtlib.map_option freshen_term t in 
   let freshen_capture_variables = List.map freshen_capture_variable in
   match obj with
-  | NotationPt.Inductive (params, indtypes) ->
+  | NotationPt.Inductive (params, indtypes, attrs) ->
       let indtypes =
         List.map
           (fun (n, co, ty, ctors) -> (n, co, ty, freshen_name_ty ctors))
           indtypes
       in
-      NotationPt.Inductive (freshen_capture_variables params, indtypes)
+      NotationPt.Inductive (freshen_capture_variables params, indtypes, attrs)
   | NotationPt.Theorem (n, t, ty_opt, attrs) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
       NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
-  | NotationPt.Record (params, n, ty, fields) ->
+  | NotationPt.Record (params, n, ty, fields, attrs) ->
       NotationPt.Record (freshen_capture_variables params, n,
-        freshen_term ty, freshen_name_ty_b fields)
+        freshen_term ty, freshen_name_ty_b fields, attrs)
   | NotationPt.LetRec (kind, definitions, attrs) ->
       let definitions =
         List.map
diff --git a/matita/components/content_pres/cicNotationParser.ml b/matita/components/content_pres/cicNotationParser.ml
index df0a781c0..1e6860281 100644
--- a/matita/components/content_pres/cicNotationParser.ml
+++ b/matita/components/content_pres/cicNotationParser.ml
@@ -657,7 +657,8 @@ EXTEND
         args = LIST1 arg;
         index_name = OPT [ "on"; id = single_arg -> id ];
         ty = OPT [ SYMBOL ":" ; p = term -> p ];
-        SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+        opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+          let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
           let rec position_of name p = function 
             | [] -> None, p
             | n :: _ when n = name -> Some p, p
@@ -695,7 +696,8 @@ EXTEND
         name = single_arg;
         args = LIST0 arg;
         ty = OPT [ SYMBOL ":" ; p = term -> p ];
-        SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+        opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+          let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
           let args =
            List.concat
             (List.map
diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 58e600a42..f27c723b0 100644
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -315,7 +315,7 @@ let domain_of_obj ~context ast =
       @ (match bo with
           None -> []
         | Some bo -> domain_of_term [] bo)
-   | Ast.Inductive (params,tyl) ->
+   | Ast.Inductive (params,tyl,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->
@@ -335,7 +335,7 @@ let domain_of_obj ~context ast =
                List.map
                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
                 tyl)
-   | Ast.Record (params,var,ty,fields) ->
+   | Ast.Record (params,var,ty,fields,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->
diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 25024f26d..91086b46d 100644
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -58,12 +58,12 @@ let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
 
 let default_associativity = Gramext.NonA
         
-let mk_rec_corec src ind_kind defs loc = 
- let attrs = src, `Definition, `Regular in
+let mk_rec_corec src flavour ind_kind defs loc = 
+ let attrs = src, flavour, `Regular in
   (loc, N.LetRec (ind_kind, defs, attrs))
 
-let nmk_rec_corec src ind_kind defs loc index = 
- let loc,t = mk_rec_corec src ind_kind defs loc in
+let nmk_rec_corec src flavour ind_kind defs loc index = 
+ let loc,t = mk_rec_corec src flavour ind_kind defs loc in
   G.NObj (loc,t,index)
 
 let shift_vars binder (vars, ty) bo =
@@ -529,27 +529,33 @@ EXTEND
     | src = source; IDENT "axiom"; i = index; name = IDENT; SYMBOL ":"; typ = term ->
         let attrs = src, `Axiom, `Regular in
 	G.NObj (loc, N.Theorem (name, typ, None, attrs),i)
-    | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
-    | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
-      paramspec = OPT inverter_param_list ; 
-      outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
-        G.NInverter (loc,name,indty,paramspec,outsort)
-    | src = source; LETCOREC ; defs = let_codefs -> 
-        nmk_rec_corec src `CoInductive defs loc true
-    | src = source; LETREC ; defs = let_defs -> 
-        nmk_rec_corec src `Inductive defs loc true
-(* FG: no source since no i_attr in N.Inductive *)
-    | IDENT "inductive"; spec = inductive_spec ->
+    | src = source; IDENT "inductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
-        G.NObj (loc, N.Inductive (params, ind_types),true)
-(* FG: no source since no i_attr in N.Inductive *)
-    | IDENT "coinductive"; spec = inductive_spec ->
+        G.NObj (loc, N.Inductive (params, ind_types, src),true)
+    | src = source; IDENT "coinductive"; spec = inductive_spec ->
         let (params, ind_types) = spec in
         let ind_types = (* set inductive flags to false (coinductive) *)
           List.map (fun (name, _, term, ctors) -> (name, false, term, ctors))
             ind_types
         in
-        G.NObj (loc, N.Inductive (params, ind_types),true)
+        G.NObj (loc, N.Inductive (params, ind_types, src),true)
+    | src = source; IDENT "record" ; (params,name,ty,fields) = record_spec ->
+        G.NObj (loc, N.Record (params,name,ty,fields,src),true)
+(* FG: new syntax for inductive/coinductive definitions and statements *)
+    | src = source; IDENT "rec"; nflavour = ntheorem_flavour; defs = let_defs -> 
+        nmk_rec_corec src nflavour `Inductive defs loc true
+    | src = source; IDENT "corec"; nflavour = ntheorem_flavour; defs = let_codefs ->
+        nmk_rec_corec src nflavour `CoInductive defs loc true
+(**)
+    | LETCOREC ; defs = let_codefs -> 
+        nmk_rec_corec `Provided `Definition `CoInductive defs loc true
+    | LETREC ; defs = let_defs -> 
+        nmk_rec_corec `Provided `Definition `Inductive defs loc true
+    | IDENT "discriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
+    | IDENT "inverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
+      paramspec = OPT inverter_param_list ; 
+      outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
+        G.NInverter (loc,name,indty,paramspec,outsort)
     | IDENT "universe"; IDENT "constraint"; u1 = tactic_term; 
         SYMBOL <:unicode<lt>> ; u2 = tactic_term ->
         let urify = function 
@@ -570,9 +576,6 @@ EXTEND
         "to"; target = term -> t,ty,(id,source),target ] ->
           let compose = compose = None in
           G.NCoercion(loc,name,compose,spec)
-(* FG: no source since no i_attr in N.Record *)
-    | IDENT "record" ; (params,name,ty,fields) = record_spec ->
-        G.NObj (loc, N.Record (params,name,ty,fields),true)
     | IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with"; 
       m = LIST0 [ u1 = URI; SYMBOL <:unicode<mapsto>>; u2 = URI -> u1,u2 ] ->
         G.NCopy (loc,s,NUri.uri_of_string u,
diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index e2c8c76d0..47b1ac063 100644
--- a/matita/components/ng_cic_content/interpretations.ml
+++ b/matita/components/ng_cic_content/interpretations.ml
@@ -646,9 +646,9 @@ let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) =
 	    | None    -> None
 	 in
 	 N.Theorem (n, ty, xbo, attrs)
-      | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->      
+      | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) ->      
          let captures, context = build_captures lno itl in
-	 N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)
+	 N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src)
       | _ -> assert false  (* NCic.Fixpoint (is_rec, ifl, _) -> *)
 
 let nmap_obj status = with_idrefs nmap_obj0 status
diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index baa28b2d6..9cfbbc8c0 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -248,8 +248,8 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
    in
    let name = 
      match obj with
-     | NotationPt.Inductive (_,(name,_,_,_)::_)
-     | NotationPt.Record (_,name,_,_) -> name ^ ".ind"
+     | NotationPt.Inductive (_,(name,_,_,_)::_,_)
+     | NotationPt.Record (_,name,_,_,_) -> name ^ ".ind"
      | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
      | NotationPt.LetRec (_,(_,(NotationPt.Ident (name, None),_),_,_)::_,_) -> name ^ ".con"
      | NotationPt.LetRec _
diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml
index 24e69a43d..5c0d0a7d5 100644
--- a/matita/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml
@@ -439,7 +439,7 @@ let interpretate_obj status
              ~obj_context:[] ~context:[] ~env ~uri:None ~is_path:false bo
           in
           NCic.Constant ([],name,Some bo,ty',attrs))
- | NotationPt.Inductive (params,tyl) ->
+ | NotationPt.Inductive (params,tyl,source) ->
     let context,params =
      let context,res =
       List.fold_left
@@ -492,10 +492,10 @@ let interpretate_obj status
       ) tyl
     in
      let height = (* XXX calculate *) 0 in
-     let attrs = `Provided, `Regular in
+     let attrs = source, `Regular in
      uri, height, [], [], 
      NCic.Inductive (inductive,leftno,tyl,attrs)
- | NotationPt.Record (params,name,ty,fields) ->
+ | NotationPt.Record (params,name,ty,fields,source) ->
     let context,params =
      let context,res =
       List.fold_left
@@ -546,7 +546,7 @@ let interpretate_obj status
     let tyl = [relevance,name,ty',[relevance,"mk_" ^ name,con']] in
     let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
      let height = (* XXX calculate *) 0 in
-     let attrs = `Provided, `Record field_names in
+     let attrs = source, `Record field_names in
      uri, height, [], [], 
      NCic.Inductive (true,leftno,tyl,attrs)
  | NotationPt.LetRec (kind, defs, attrs) ->
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
index dc9c4498e..b60a87aef 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma
@@ -66,7 +66,7 @@ definition cfun: candidate → candidate → candidate ≝
                  ⬇*[Ⓕ, cs] L ≡ K → ⬆*[cs] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
 
 (* the reducibility candidate associated to an atomic arity *)
-let rec acr (RP:candidate) (A:aarity) on A: candidate ≝
+rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝
 match A with
 [ AAtom     ⇒ RP
 | APair B A ⇒ cfun (acr RP B) (acr RP A)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
index 29fee0ef1..f608f8c3c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
@@ -16,7 +16,7 @@ include "basic_2/grammar/lenv.ma".
 
 (* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
 
-let rec length L ≝ match L with
+rec definition length L ≝ match L with
 [ LAtom       ⇒ 0
 | LPair L _ _ ⇒ ⫯(length L)
 ].
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
index 9bd6e8260..c9d79e5f5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_weight.ma
@@ -17,7 +17,7 @@ include "basic_2/grammar/lenv.ma".
 
 (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
 
-let rec lw L ≝ match L with
+rec definition lw L ≝ match L with
 [ LAtom       ⇒ 0
 | LPair L _ V ⇒ lw L + ♯{V}
 ].
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma
index 192b78637..1dbfd8f64 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma
@@ -18,7 +18,7 @@ include "basic_2/grammar/term_simple.ma".
 
 (* TERMS ********************************************************************)
 
-let rec applv Vs T on Vs ≝
+rec definition applv Vs T on Vs ≝
   match Vs with
   [ nil        ⇒ T
   | cons hd tl ⇒ ⓐhd. (applv tl T)
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 3787abe93..23659262d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_weight.ma
@@ -17,7 +17,7 @@ include "basic_2/grammar/term.ma".
 
 (* WEIGHT OF A TERM *********************************************************)
 
-let rec tw T ≝ match T with
+rec definition tw T ≝ match T with
 [ TAtom _     ⇒ 1
 | TPair _ V T ⇒ tw V + tw T + 1
 ].
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
index a16d19042..2bf43b5ee 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
@@ -84,7 +84,7 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
 ]
 defined.
 
-let rec sd_d (h:sh) (k:nat) (d:nat) on d : sd h ≝
+rec definition sd_d (h:sh) (k:nat) (d:nat) on d : sd h ≝
    match d with
    [ O   ⇒ sd_O h
    | S d ⇒ match d with
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 325e07d38..1ba525475 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -220,7 +220,7 @@ qed-.
 (* Iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetics/bigops.ma *)
-let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
+rec definition iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
   match n with
    [ O   ⇒ nil
    | S k ⇒ op (iter k B op nil)
@@ -249,7 +249,7 @@ qed.
 (* Trichotomy operator ******************************************************)
 
 (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
-let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
+rec definition tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝
   match n1 with
   [ O    ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ]
   | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ]
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
index 9e8d1ff41..baa9179e9 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma
@@ -26,7 +26,7 @@ interpretation "nil (list)" 'Nil = (nil ?).
 
 interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
 
-let rec length (A:Type[0]) (l:list A) on l ≝ match l with
+rec definition length (A:Type[0]) (l:list A) on l ≝ match l with
 [ nil      ⇒ 0
 | cons _ l ⇒ ⫯(length A l)
 ].
@@ -34,7 +34,7 @@ let rec length (A:Type[0]) (l:list A) on l ≝ match l with
 interpretation "length (list)"
    'card l = (length ? l).
 
-let rec all A (R:predicate A) (l:list A) on l ≝
+rec definition all A (R:predicate A) (l:list A) on l ≝
   match l with
   [ nil        ⇒ ⊤
   | cons hd tl ⇒ R hd ∧ all A R tl
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
index f73099445..b9a7327de 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma
@@ -27,7 +27,7 @@ interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?).
 
 interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
 
-let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
+rec definition append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
 [ nil2           ⇒ l2
 | cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2
 ].
@@ -35,7 +35,7 @@ let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
 interpretation "append (list of pairs)"
    'Append l1 l2 = (append2 ? ? l1 l2).
 
-let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
+rec definition length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with
 [ nil2        ⇒ 0
 | cons2 _ _ l ⇒ ⫯(length2 A1 A2 l)
 ].
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma
index 839811603..9435b5010 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_eq.ma
@@ -44,11 +44,11 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-let corec eq_stream_refl: ∀A. reflexive … (eq_stream A) ≝ ?.
+corec lemma eq_stream_refl: ∀A. reflexive … (eq_stream A).
 #A * #b #t @eq_seq //
 qed.
 
-let corec eq_stream_sym: ∀A. symmetric … (eq_stream A) ≝ ?.
+corec lemma eq_stream_sym: ∀A. symmetric … (eq_stream A).
 #A #t1 #t2 * -t1 -t2
 #t1 #t2 #b1 #b2 #Hb #Ht @eq_seq /2 width=1 by/
 qed-.
@@ -58,7 +58,7 @@ lemma eq_stream_repl_sym: ∀A,R. eq_stream_repl_back A R → eq_stream_repl_fwd
 
 (* Main properties **********************************************************)
 
-let corec eq_stream_trans: ∀A. Transitive … (eq_stream A) ≝ ?.
+corec theorem eq_stream_trans: ∀A. Transitive … (eq_stream A).
 #A #t1 #t * -t1 -t
 #t1 #t #b1 #b * #Ht1 * #b2 #t2 #H cases (eq_stream_inv_seq A … H) -H -b
 /3 width=7 by eq_seq/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma
index 96b9abe98..d2d6bcc30 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/streams_tls.ma
@@ -17,9 +17,9 @@ include "ground_2/lib/streams_hdtl.ma".
 
 (* STREAMS ******************************************************************)
 
-let rec tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
+rec definition tls (A:Type[0]) (n:nat) on n: stream A → stream A ≝ ?.
 cases n -n [ #t @t | #n #t @tl @(tls … n t) ]
-qed.
+defined.
 
 interpretation "recursive tail (strams)" 'Drops n f = (tls ? n f).
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
index 11ffaa407..da3380da9 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma
@@ -16,7 +16,7 @@ include "ground_2/relocation/mr2.ma".
 
 (* MULTIPLE RELOCATION WITH PAIRS *******************************************)
 
-let rec pluss (cs:mr2) (i:nat) on cs ≝ match cs with
+rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with
 [ nil2         ⇒ ◊
 | cons2 l m cs ⇒ {l + i, m} @ pluss cs i
 ].
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
index 8d7dacc4e..c852317f8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream.ma
@@ -25,7 +25,7 @@ interpretation "push (nstream)" 'Lift f = (push f).
 
 definition next: rtmap → rtmap.
 * #n #f @(⫯n@f)
-qed.
+defined.
 
 interpretation "next (nstream)" 'Successor f = (next f).
 
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
index a9b022b4d..f8b71a6a5 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_after.ma
@@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_after.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-let corec compose: rtmap → rtmap → rtmap ≝ ?.
+corec definition compose: rtmap → rtmap → rtmap.
 #f1 * #n2 #f2 @(seq … (f1@❴n2❵)) @(compose ? f2) -compose -f2
 @(↓*[⫯n2] f1)
 defined.
@@ -81,7 +81,7 @@ lemma after_apply: ∀n2,f1,f2,f. (↓*[⫯n2] f1) ⊚ f2 ≡ f → f1 ⊚ n2@f2
 ]
 qed-.
 
-let corec after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f ≝ ?.
+corec lemma after_total_aux: ∀f1,f2,f. f1 ∘ f2 = f → f1 ⊚ f2 ≡ f.
 * #n1 #f1 * #n2 #f2 * #n #f cases n1 -n1
 [ cases n2 -n2
   [ #H cases (compose_inv_O2 … H) -H /3 width=7 by after_refl, eq_f2/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
index 4d979cefb..1b6c466ba 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_eq.ma
@@ -32,7 +32,7 @@ lemma eq_inv_seq: ∀g1,g2. g1 ≗ g2 → ∀f1,f2,n1,n2. n1@f1 = g1 → n2@f2 =
                   n1 = n2 ∧ f1 ≗ f2.
 /2 width=1 by eq_inv_seq_aux/ qed-.
 
-let corec nstream_eq: ∀f1,f2. f1 ≗ f2 → f1 ≐ f2 ≝ ?.
+corec lemma nstream_eq: ∀f1,f2. f1 ≗ f2 → f1 ≐ f2.
 * #n1 #f1 * #n2 #f2 #Hf cases (eq_inv_gen … Hf) -Hf *
 #g1 #g2 #Hg #H1 #H2
 [ cases (push_inv_seq_dx … H1) -H1 * -n1 #H1
@@ -45,7 +45,7 @@ let corec nstream_eq: ∀f1,f2. f1 ≗ f2 → f1 ≐ f2 ≝ ?.
 ]
 qed-.
 
-let corec nstream_inv_eq: ∀f1,f2. f1 ≐ f2 → f1 ≗ f2 ≝ ?.
+corec lemma nstream_inv_eq: ∀f1,f2. f1 ≐ f2 → f1 ≗ f2.
 * #n1 #f1 * #n2 #f2 #H cases (eq_stream_inv_seq ??? H) -H [2,3,4,5,6,7: // ]
 #Hf * -n2 cases n1 -n1 /3 width=5 by eq_push/
 #n @eq_next /3 width=5 by eq_seq/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
index 11307fbd2..28d0e02f0 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_id.ma
@@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_eq.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-let corec id: rtmap ≝ ↑id.
+corec definition id: rtmap ≝ ↑id.
 
 interpretation "identity (nstream)"
    'Identity = (id).
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
index d2bd0837e..0bf3c4da8 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma
@@ -18,7 +18,7 @@ include "ground_2/relocation/rtmap_istot.ma".
 
 (* RELOCATION N-STREAM ******************************************************)
 
-let rec apply (i: nat) on i: rtmap → nat ≝ ?.
+rec definition apply (i: nat) on i: rtmap → nat ≝ ?.
 * #n #f cases i -i
 [ @n
 | #i lapply (apply i f) -apply -i -f
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
index cdded4f97..3db5d524f 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -161,7 +161,7 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-let corec after_eq_repl_back_2:  ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≡ f) ≝ ?.
+corec lemma after_eq_repl_back_2: ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≡ f).
 #f1 #f #f2 * -f2 -f1 -f
 #f21 #f1 #f #g21 [1,2: #g1 ] #g #Hf #H21 [1,2: #H1 ] #H #g22 #H0
 [ cases (eq_inv_px …  H0 …  H21) -g21 /3 width=7 by after_refl/
@@ -170,11 +170,11 @@ let corec after_eq_repl_back_2:  ∀f1,f. eq_repl_back (λf2. f2 ⊚ f1 ≡ f) 
 ]
 qed-.
 
-lemma after_eq_repl_fwd_2:  ∀f1,f. eq_repl_fwd (λf2. f2 ⊚ f1 ≡ f).
+lemma after_eq_repl_fwd_2: ∀f1,f. eq_repl_fwd (λf2. f2 ⊚ f1 ≡ f).
 #f1 #f @eq_repl_sym /2 width=3 by after_eq_repl_back_2/
 qed-.
 
-let corec after_eq_repl_back_1:  ∀f2,f. eq_repl_back (λf1. f2 ⊚ f1 ≡ f) ≝ ?.
+corec lemma after_eq_repl_back_1: ∀f2,f. eq_repl_back (λf1. f2 ⊚ f1 ≡ f).
 #f2 #f #f1 * -f2 -f1 -f
 #f2 #f11 #f #g2 [1,2: #g11 ] #g #Hf #H2 [1,2: #H11 ] #H #g2 #H0
 [ cases (eq_inv_px …  H0 …  H11) -g11 /3 width=7 by after_refl/
@@ -183,11 +183,11 @@ let corec after_eq_repl_back_1:  ∀f2,f. eq_repl_back (λf1. f2 ⊚ f1 ≡ f) 
 ]
 qed-.
 
-lemma after_eq_repl_fwd_1:  ∀f2,f. eq_repl_fwd (λf1. f2 ⊚ f1 ≡ f).
+lemma after_eq_repl_fwd_1: ∀f2,f. eq_repl_fwd (λf1. f2 ⊚ f1 ≡ f).
 #f2 #f @eq_repl_sym /2 width=3 by after_eq_repl_back_1/
 qed-.
 
-let corec after_eq_repl_back_0:  ∀f1,f2. eq_repl_back (λf. f2 ⊚ f1 ≡ f) ≝ ?.
+corec lemma after_eq_repl_back_0: ∀f1,f2. eq_repl_back (λf. f2 ⊚ f1 ≡ f).
 #f2 #f1 #f * -f2 -f1 -f
 #f2 #f1 #f01 #g2 [1,2: #g1 ] #g01 #Hf01 #H2 [1,2: #H1 ] #H01 #g02 #H0
 [ cases (eq_inv_px …  H0 …  H01) -g01 /3 width=7 by after_refl/
@@ -196,15 +196,15 @@ let corec after_eq_repl_back_0:  ∀f1,f2. eq_repl_back (λf. f2 ⊚ f1 ≡ f) 
 ]
 qed-.
 
-lemma after_eq_repl_fwd_0:  ∀f2,f1. eq_repl_fwd (λf. f2 ⊚ f1 ≡ f).
+lemma after_eq_repl_fwd_0: ∀f2,f1. eq_repl_fwd (λf. f2 ⊚ f1 ≡ f).
 #f2 #f1 @eq_repl_sym /2 width=3 by after_eq_repl_back_0/
 qed-.
 
 (* Main properties **********************************************************)
 
-let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
-                        ∀f1,f2. f1 ⊚ f2 ≡ f0 →
-                        ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?.
+corec theorem after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
+                            ∀f1,f2. f1 ⊚ f2 ≡ f0 →
+                            ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4.
 #f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
 [ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
   cases (after_inv_xxp … Hg0 … H0) -g0
@@ -226,9 +226,9 @@ let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
 ]
 qed-.
 
-let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
-                        ∀f2, f3. f2 ⊚ f3 ≡ f0 →
-                        ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?.
+corec theorem after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
+                            ∀f2, f3. f2 ⊚ f3 ≡ f0 →
+                            ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4.
 #f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
 [ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
   cases (after_inv_xxp … Hg0 … H0) -g0
@@ -252,7 +252,7 @@ qed-.
 
 (* Main inversion lemmas on after *******************************************)
 
-let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y ≝ ?.
+corec theorem after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y.
 #f1 #f2 #x #y * -f1 -f2 -x
 #f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
 [ cases (after_inv_ppx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_push/
@@ -276,12 +276,12 @@ qed.
 
 (* Inversion lemmas on isid *************************************************)
 
-let corec isid_after_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊚ f2 ≡ f2 ≝ ?.
+corec lemma isid_after_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊚ f2 ≡ f2.
 #f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * #g2 #H2
 /3 width=7 by after_push, after_refl/
 qed-.
 
-let corec isid_after_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⊚ f2 ≡ f1 ≝ ?.
+corec lemma isid_after_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⊚ f2 ≡ f1.
 #f2 * -f2 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * #g1 #H1
 [ /3 width=7 by after_refl/
 | @(after_next … H1 H1) /3 width=3 by isid_push/
@@ -296,14 +296,14 @@ lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f →  𝐈⦃f2⦄ → f1 
 /3 width=6 by isid_after_dx, after_mono/
 qed-.
 
-let corec after_fwd_isid1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ≝ ?.
+corec lemma after_fwd_isid1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄.
 #f1 #f2 #f * -f1 -f2 -f
 #f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H
 [ /4 width=6 by isid_inv_push, isid_push/ ]
 cases (isid_inv_next … H … H0)
 qed-.
 
-let corec after_fwd_isid2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f2⦄ ≝ ?.
+corec lemma after_fwd_isid2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f2⦄.
 #f1 #f2 #f * -f1 -f2 -f
 #f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H
 [ /4 width=6 by isid_inv_push, isid_push/ ]
@@ -419,7 +419,7 @@ lemma after_fwd_isid_dx: ∀f2,f1,f.  𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f2 ≗
 /3 width=8 by at_inj, at_eq_repl_back/
 qed-.
 
-let corec after_inj_O_aux: ∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1 ≝ ?.
+corec fact after_inj_O_aux: ∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1.
 #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
 cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1
 lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
index 00ee4edb2..e60a2affc 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_at.ma
@@ -183,7 +183,7 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-let corec at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2) ≝ ?.
+corec lemma at_eq_repl_back: ∀i1,i2. eq_repl_back (λf. @⦃i1, f⦄ ≡ i2).
 #i1 #i2 #f1 #H1 cases H1 -f1 -i1 -i2
 [ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /2 width=2 by at_refl/
 | #f1 #i1 #i2 #Hf1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12 cases (eq_inv_px … H12 … H) -g1 /3 width=7 by at_push/
@@ -286,9 +286,9 @@ qed.
 lemma isid_inv_at_mono: ∀f,i1,i2. 𝐈⦃f⦄ → @⦃i1, f⦄ ≡ i2 → i1 = i2.
 /3 width=6 by isid_inv_at, at_mono/ qed-.
 
-(* Advancedd properties on isid *********************************************)
+(* Advanced properties on isid **********************************************)
 
-let corec isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄ ≝ ?.
+corec lemma isid_at: ∀f. (∀i. @⦃i, f⦄ ≡ i) → 𝐈⦃f⦄.
 #f #Hf lapply (Hf 0)
 #H cases (at_fwd_id_ex … H) -H
 #g #H @(isid_push … H) /3 width=7 by at_inv_npn/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
index 4430c2f8a..8f0f5d0df 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_eq.ma
@@ -36,12 +36,12 @@ definition eq_repl_fwd (R:predicate …) ≝
 
 (* Basic properties *********************************************************)
 
-let corec eq_refl: reflexive … eq ≝ ?.
+corec lemma eq_refl: reflexive … eq.
 #f cases (pn_split f) *
 #g #Hg [ @(eq_push … Hg Hg) | @(eq_next … Hg Hg) ] -Hg //
 qed.
 
-let corec eq_sym: symmetric … eq ≝ ?.
+corec lemma eq_sym: symmetric … eq.
 #f1 #f2 * -f1 -f2
 #f1 #f2 #g1 #g2 #Hf #H1 #H2
 [ @(eq_push … H2 H1) | @(eq_next … H2 H1) ] -g2 -g1 /2 width=1 by/
@@ -129,7 +129,7 @@ qed-.
 
 (* Main properties **********************************************************)
 
-let corec eq_trans: Transitive … eq ≝ ?.
+corec theorem eq_trans: Transitive … eq.
 #f1 #f * -f1 -f
 #f1 #f #g1 #g #Hf1 #H1 #H #f2 #Hf2
 [ cases (eq_inv_px … Hf2 … H) | cases (eq_inv_nx … Hf2 … H) ] -g
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
index 5ad6aa83c..7dde16d0f 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isid.ma
@@ -43,7 +43,9 @@ lemma isid_inv_next: ∀g. 𝐈⦃g⦄ → ∀f. ⫯f = g → ⊥.
 #f #Hf * -g #g #H elim (discr_next_push … H)
 qed-.
 
-let corec isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≗ f2 ≝ ?.
+(* Main inversion lemmas ****************************************************)
+
+corec theorem isid_inv_eq_repl: ∀f1,f2. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → f1 ≗ f2.
 #f1 #f2 #H1 #H2
 cases (isid_inv_gen … H1) -H1
 cases (isid_inv_gen … H2) -H2
@@ -52,7 +54,7 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-let corec isid_eq_repl_back: eq_repl_back … isid ≝ ?.
+corec lemma isid_eq_repl_back: eq_repl_back … isid.
 #f1 #H cases (isid_inv_gen … H) -H
 #g1 #Hg1 #H1 #f2 #Hf cases (eq_inv_px … Hf … H1) -f1
 /3 width=3 by isid_push/
@@ -63,11 +65,11 @@ lemma isid_eq_repl_fwd: eq_repl_fwd … isid.
 
 (* Alternative definition ***************************************************)
 
-let corec eq_push_isid: ∀f. ↑f ≗ f → 𝐈⦃f⦄ ≝ ?.
+corec lemma eq_push_isid: ∀f. ↑f ≗ f → 𝐈⦃f⦄.
 #f #H cases (eq_inv_px … H) -H /4 width=3 by isid_push, eq_trans/
 qed.
 
-let corec eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f ≝ ?.
+corec lemma eq_push_inv_isid: ∀f. 𝐈⦃f⦄ → ↑f ≗ f.
 #f * -f
 #f #g #Hf #Hg @(eq_push … Hg) [2: @eq_push_inv_isid // | skip ]
 @eq_f //
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
index d4e80390f..561a8ef6b 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_istot.ma
@@ -47,10 +47,11 @@ lemma istot_tls: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃⫱*[n]f⦄.
 #n elim n -n /3 width=1 by istot_tl/
 qed.
 
-(* Advanced forward lemmas on at ********************************************)
+(* Main forward lemmas on at ************************************************)
 
-let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ →
-                  (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) → f1 ≗ f2 ≝ ?.
+corec theorem at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ →
+                      (∀i,i1,i2. @⦃i, f1⦄ ≡ i1 → @⦃i, f2⦄ ≡ i2 → i1 = i2) →
+                      f1 ≗ f2.
 #f1 cases (pn_split f1) * #g1 #H1
 #f2 cases (pn_split f2) * #g2 #H2
 #Hf1 #Hf2 #Hi
@@ -69,7 +70,7 @@ let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ →
 ]
 qed-.
 
-(* Main properties on at ****************************************************)
+(* Advanced properties on at ************************************************)
 
 lemma at_dec: ∀f,i1,i2. 𝐓⦃f⦄ → Decidable (@⦃i1, f⦄ ≡ i2).
 #f #i1 #i2 #Hf lapply (Hf i1) -Hf *
@@ -79,7 +80,8 @@ lemma at_dec: ∀f,i1,i2. 𝐓⦃f⦄ → Decidable (@⦃i1, f⦄ ≡ i2).
 ]
 qed-.
 
-lemma is_at_dec_le: ∀f,i2,i. 𝐓⦃f⦄ → (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) → Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
+lemma is_at_dec_le: ∀f,i2,i. 𝐓⦃f⦄ → (∀i1. i1 + i ≤ i2 → @⦃i1, f⦄ ≡ i2 → ⊥) →
+                    Decidable (∃i1. @⦃i1, f⦄ ≡ i2).
 #f #i2 #i #Hf elim i -i
 [ #Ht @or_intror * /3 width=3 by at_increasing/
 | #i #IH #Ht elim (at_dec f (i2-i) i2) /3 width=2 by ex_intro, or_introl/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma
index 5f707a571..86ad267c6 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sand.ma
@@ -73,12 +73,12 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-let corec sand_refl: ∀f. f ⋒ f ≡ f ≝ ?.
+corec lemma sand_refl: ∀f. f ⋒ f ≡ f.
 #f cases (pn_split f) * #g #H
 [ @(sand_pp … H H H) | @(sand_nn … H H H) ] -H //
 qed.
 
-let corec sand_sym: ∀f1,f2,f. f1 ⋒ f2 ≡ f → f2 ⋒ f1 ≡ f ≝ ?.
+corec lemma sand_sym: ∀f1,f2,f. f1 ⋒ f2 ≡ f → f2 ⋒ f1 ≡ f.
 #f1 #f2 #f * -f1 -f2 -f
 #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
 [ @sand_pp | @sand_pn | @sand_np | @sand_nn ] /2 width=7 by/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
index b27488644..616460173 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
@@ -67,7 +67,7 @@ qed-.
 
 (* properties on isid *******************************************************)
 
-let corec sle_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊆ f2 ≝ ?.
+corec lemma sle_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊆ f2.
 #f1 * -f1
 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) *
 /3 width=5 by sle_weak, sle_push/
@@ -75,7 +75,7 @@ qed.
 
 (* inversion lemmas on isid *************************************************)
 
-let corec sle_inv_isid_dx: ∀f1,f2. f1 ⊆ f2 → 𝐈⦃f2⦄ → 𝐈⦃f1⦄ ≝ ?.
+corec lemma sle_inv_isid_dx: ∀f1,f2. f1 ⊆ f2 → 𝐈⦃f2⦄ → 𝐈⦃f1⦄.
 #f1 #f2 * -f1 -f2
 #f1 #f2 #g1 #g2 #Hf * * #H
 [2,3: elim (isid_inv_next … H) // ]
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
index 7b437099e..9b093603c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -73,12 +73,12 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-let corec sor_refl: ∀f. f ⋓ f ≡ f ≝ ?.
+corec lemma sor_refl: ∀f. f ⋓ f ≡ f.
 #f cases (pn_split f) * #g #H
 [ @(sor_pp … H H H) | @(sor_nn … H H H) ] -H //
 qed.
 
-let corec sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f ≝ ?.
+corec lemma sor_sym: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f2 ⋓ f1 ≡ f.
 #f1 #f2 #f * -f1 -f2 -f
 #f1 #f2 #f #g1 #g2 #g #Hf * * * -g1 -g2 -g
 [ @sor_pp | @sor_pn | @sor_np | @sor_nn ] /2 width=7 by/
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
index d46148840..11a0c9092 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_tls.ma
@@ -17,7 +17,7 @@ include "ground_2/relocation/rtmap_tl.ma".
 
 (* RELOCATION MAP ***********************************************************)
 
-let rec tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with
+rec definition tls (f:rtmap) (n:nat) on n: rtmap ≝ match n with
 [ O ⇒ f | S m ⇒ ⫱(tls f m) ].
 
 interpretation "tls (rtmap)" 'DropPreds n f = (tls f n).
diff --git a/matita/matita/lib/basics/core_notation.ma b/matita/matita/lib/basics/core_notation.ma
index dd672ee84..77e44c201 100644
--- a/matita/matita/lib/basics/core_notation.ma
+++ b/matita/matita/lib/basics/core_notation.ma
@@ -109,7 +109,7 @@ notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
   non associative with precedence 45
 for @{ 'congruent $n $m $p }.
 
-(* other notations **********************************************************)
+(* pairs, projections *******************************************************)
 
 notation "hvbox(\langle term 19 a, break term 19 b\rangle)" 
 with precedence 90 for @{ 'pair $a $b}.
@@ -126,6 +126,8 @@ notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b
 notation > "\fst" with precedence 90 for @{'pi1}.
 notation > "\snd" with precedence 90 for @{'pi2}.
 
+(* implication **************************************************************)
+
 notation "hvbox(a break \to b)" 
   right associative with precedence 20
 for @{ \forall $_:$a.$b }.
@@ -134,6 +136,8 @@ notation < "hvbox(a break \to b)"
   right associative with precedence 20
 for @{ \Pi $_:$a.$b }.
 
+(* orders *******************************************************************)
+
 notation "hvbox(a break \leq b)" 
   non associative with precedence 45
 for @{ 'leq $a $b }.
@@ -150,6 +154,8 @@ notation "hvbox(a break \gt b)"
   non associative with precedence 45
 for @{ 'gt $a $b }.
 
+(* negated equality *********************************************************)
+
 notation > "hvbox(a break \neq b)" 
   non associative with precedence 45
 for @{ 'neq ? $a $b }.
@@ -158,6 +164,8 @@ notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
   non associative with precedence 45
 for @{ 'neq $t $a $b }.
 
+(* negated orders ***********************************************************)
+
 notation "hvbox(a break \nleq b)" 
   non associative with precedence 45
 for @{ 'nleq $a $b }.
@@ -174,6 +182,8 @@ notation "hvbox(a break \ngtr b)"
   non associative with precedence 45
 for @{ 'ngtr $a $b }.
 
+(* divides, negated divides *************************************************)
+
 notation "hvbox(a break \divides b)"
   non associative with precedence 45
 for @{ 'divides $a $b }.
@@ -182,6 +192,8 @@ notation "hvbox(a break \ndivides b)"
   non associative with precedence 45
 for @{ 'ndivides $a $b }.
 
+(* arithmetics **************************************************************)
+
 notation "hvbox(a break + b)" 
   left associative with precedence 55
 for @{ 'plus $a $b }.
@@ -225,6 +237,8 @@ notation "\sqrt a"
   non associative with precedence 65
 for @{ 'sqrt $a }.
 
+(* logical connectives ******************************************************)
+
 notation "hvbox(a break \lor b)" 
   left associative with precedence 30
 for @{ 'or $a $b }.
@@ -245,6 +259,7 @@ notation "hvbox(a break \leftrightarrow b)"
   left associative with precedence 25
 for @{ 'iff $a $b }.
 
+(* subsets ******************************************************************)
 
 notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
 for @{ 'powerset $A }.
@@ -283,6 +298,8 @@ for @{ 'union $a $b }. (* \cup *)
 
 notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
 
+(* other notations **********************************************************)
+
 notation "hvbox(a break \approx b)" non associative with precedence 45 
   for @{ 'napart $a $b}.
         
diff --git a/matita/matita/lib/fail.txt b/matita/matita/lib/fail.txt
new file mode 100644
index 000000000..4330dddb1
--- /dev/null
+++ b/matita/matita/lib/fail.txt
@@ -0,0 +1,27 @@
+matitac.opt turing/multi_to_mono/multi_to_mono.maFAIL 0m00.54s 0m00.52s 0m00.01s 
+matitac.opt binding/names.ma                     FAIL 0m00.07s 0m00.07s 0m00.00s 
+matitac.opt binding/fp.ma
+ matitac.opt binding/names.ma                    FAIL 0m00.12s 0m00.12s 0m00.00s 
+matitac.opt binding/fp.ma                        FAIL 0m00.13s 0m00.12s 0m00.00s 
+matitac.opt binding/ln.ma
+ matitac.opt binding/names.ma                    FAIL 0m00.07s 0m00.07s 0m00.00s 
+matitac.opt binding/ln.ma                        FAIL 0m00.43s 0m00.43s 0m00.00s 
+matitac.opt binding/ln_concrete.ma
+ matitac.opt binding/names.ma                    FAIL 0m00.06s 0m00.06s 0m00.00s 
+matitac.opt binding/ln_concrete.ma               FAIL 0m00.49s 0m00.48s 0m00.00s 
+matitac.opt finite_lambda/reduction.ma
+ matitac.opt finite_lambda/terms_and_types.ma    FAIL 0m00.47s 0m00.47s 0m00.00s 
+matitac.opt finite_lambda/reduction.ma           FAIL 0m00.48s 0m00.47s 0m00.00s 
+matitac.opt finite_lambda/typing.ma
+ matitac.opt finite_lambda/reduction.ma
+  matitac.opt finite_lambda/terms_and_types.ma   FAIL 0m00.39s 0m00.39s 0m00.00s 
+ matitac.opt finite_lambda/reduction.ma          FAIL 0m00.39s 0m00.39s 0m00.00s 
+matitac.opt finite_lambda/typing.ma              FAIL 0m00.39s 0m00.39s 0m00.00s 
+matitac.opt finite_lambda/confluence.ma
+ matitac.opt finite_lambda/reduction.ma
+  matitac.opt finite_lambda/terms_and_types.ma   FAIL 0m00.42s 0m00.41s 0m00.00s 
+ matitac.opt finite_lambda/reduction.ma          FAIL 0m00.42s 0m00.42s 0m00.00s 
+matitac.opt finite_lambda/confluence.ma          FAIL 0m00.42s 0m00.42s 0m00.00s 
+matitac.opt finite_lambda/terms_and_types.ma     FAIL 0m00.38s 0m00.38s 0m00.00s 
+matitac.opt reverse_complexity/toolkit.ma        FAIL 0m14.70s 0m14.62s 0m00.07s 
+matitac.opt reverse_complexity/hierarchy.ma      FAIL 0m00.71s 0m00.70s 0m00.00s 
diff --git a/matita/matita/lib/inconsistent.ma b/matita/matita/lib/inconsistent.ma
new file mode 100644
index 000000000..efac1e02c
--- /dev/null
+++ b/matita/matita/lib/inconsistent.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basics/logic.ma".
+
+axiom boh: (False → False) = True.
+
+definition J: False → False ≝ λf. match f in False with [ ].
+
+definition I2: True ≝ match boh with [ refl ⇒ J ].
+
+let rec err (u: True): False ≝ match u with [ I ⇒ err I2 ].
+
+lemma oops: False ≝ err I.
diff --git a/matita/matita/matita.lang b/matita/matita/matita.lang
index ea9a08e13..136efe573 100644
--- a/matita/matita/matita.lang
+++ b/matita/matita/matita.lang
@@ -84,7 +84,6 @@
          <keyword>definition</keyword>
          <keyword>inductive</keyword>
          <keyword>coinductive</keyword>
-         <keyword>let</keyword>
          <keyword>fact</keyword>
 	 <keyword>lemma</keyword>
          <keyword>remark</keyword>