From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Mon, 16 Nov 2009 17:09:31 +0000 (+0000)
Subject: Implementation of ndestruct tactic (including destruction of constructor forms
X-Git-Tag: make_still_working~3207
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce;p=helm.git

Implementation of ndestruct tactic (including destruction of constructor forms
in the dependently typed case; not including discrimination of cycles).
---

diff --git a/helm/software/components/acic_content/.depend.opt b/helm/software/components/acic_content/.depend.opt
index 307fceaa0..fef879256 100644
--- a/helm/software/components/acic_content/.depend.opt
+++ b/helm/software/components/acic_content/.depend.opt
@@ -1,4 +1,3 @@
-content.cmi: 
 acic2content.cmi: content.cmi 
 content2cic.cmi: content.cmi 
 cicNotationUtil.cmi: cicNotationPt.cmx 
@@ -6,8 +5,6 @@ cicNotationEnv.cmi: cicNotationPt.cmx
 cicNotationPp.cmi: cicNotationPt.cmx cicNotationEnv.cmi 
 acic2astMatcher.cmi: cicNotationPt.cmx 
 termAcicContent.cmi: cicNotationPt.cmx 
-cicNotationPt.cmo: 
-cicNotationPt.cmx: 
 content.cmo: content.cmi 
 content.cmx: content.cmi 
 acic2content.cmo: content.cmi acic2content.cmi 
diff --git a/helm/software/components/acic_procedural/.depend.opt b/helm/software/components/acic_procedural/.depend.opt
index 97238c4d8..8d0128744 100644
--- a/helm/software/components/acic_procedural/.depend.opt
+++ b/helm/software/components/acic_procedural/.depend.opt
@@ -1,13 +1,6 @@
-proceduralHelpers.cmi: 
-proceduralClassify.cmi: 
-proceduralOptimizer.cmi: 
-proceduralTypes.cmi: 
-proceduralMode.cmi: 
-proceduralConversion.cmi: 
 procedural1.cmi: proceduralTypes.cmi 
 procedural2.cmi: proceduralTypes.cmi 
 proceduralTeX.cmi: proceduralTypes.cmi 
-acic2Procedural.cmi: 
 proceduralHelpers.cmo: proceduralHelpers.cmi 
 proceduralHelpers.cmx: proceduralHelpers.cmi 
 proceduralClassify.cmo: proceduralHelpers.cmi proceduralClassify.cmi 
diff --git a/helm/software/components/binaries/extractor/.depend.opt b/helm/software/components/binaries/extractor/.depend.opt
index 0c39328ae..e69de29bb 100644
--- a/helm/software/components/binaries/extractor/.depend.opt
+++ b/helm/software/components/binaries/extractor/.depend.opt
@@ -1,4 +0,0 @@
-extractor.cmo: 
-extractor.cmx: 
-extractor_manager.cmo: 
-extractor_manager.cmx: 
diff --git a/helm/software/components/binaries/table_creator/.depend.opt b/helm/software/components/binaries/table_creator/.depend.opt
index 33147b949..e69de29bb 100644
--- a/helm/software/components/binaries/table_creator/.depend.opt
+++ b/helm/software/components/binaries/table_creator/.depend.opt
@@ -1,2 +0,0 @@
-table_creator.cmo: 
-table_creator.cmx: 
diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend
index 87d1ed25c..bb6f22a64 100644
--- a/helm/software/components/binaries/transcript/.depend
+++ b/helm/software/components/binaries/transcript/.depend
@@ -1,11 +1,6 @@
 gallina8Parser.cmi: types.cmo 
 grafiteParser.cmi: types.cmo 
 grafite.cmi: types.cmo 
-engine.cmi: 
-types.cmo: 
-types.cmx: 
-options.cmo: 
-options.cmx: 
 gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi 
 gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Lexer.cmo: options.cmo gallina8Parser.cmi 
diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt
index f17459162..efadc681e 100644
--- a/helm/software/components/binaries/transcript/.depend.opt
+++ b/helm/software/components/binaries/transcript/.depend.opt
@@ -1,11 +1,6 @@
 gallina8Parser.cmi: types.cmx 
 grafiteParser.cmi: types.cmx 
 grafite.cmi: types.cmx 
-engine.cmi: 
-types.cmo: 
-types.cmx: 
-options.cmo: 
-options.cmx: 
 gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi 
 gallina8Lexer.cmo: options.cmx gallina8Parser.cmi 
diff --git a/helm/software/components/cic/.depend.opt b/helm/software/components/cic/.depend.opt
index 8cdd2a86a..76d19c1ff 100644
--- a/helm/software/components/cic/.depend.opt
+++ b/helm/software/components/cic/.depend.opt
@@ -1,10 +1,8 @@
-cicUniv.cmi: 
 unshare.cmi: cic.cmx 
 deannotate.cmi: cic.cmx 
 cicParser.cmi: cic.cmx 
 cicUtil.cmi: cic.cmx 
 helmLibraryObjects.cmi: cic.cmx 
-libraryObjects.cmi: 
 cic_indexable.cmi: cic.cmx 
 path_indexing.cmi: cic.cmx 
 cicInspect.cmi: cic.cmx 
diff --git a/helm/software/components/cic_acic/.depend.opt b/helm/software/components/cic_acic/.depend.opt
index 5449d50aa..3fc1e0dce 100644
--- a/helm/software/components/cic_acic/.depend.opt
+++ b/helm/software/components/cic_acic/.depend.opt
@@ -1,6 +1,3 @@
-eta_fixing.cmi: 
-doubleTypeInference.cmi: 
-cic2acic.cmi: 
 cic2Xml.cmi: cic2acic.cmi 
 eta_fixing.cmo: eta_fixing.cmi 
 eta_fixing.cmx: eta_fixing.cmi 
diff --git a/helm/software/components/cic_disambiguation/.depend.opt b/helm/software/components/cic_disambiguation/.depend.opt
index a9ae65a5e..e9bd1168f 100644
--- a/helm/software/components/cic_disambiguation/.depend.opt
+++ b/helm/software/components/cic_disambiguation/.depend.opt
@@ -1,5 +1,3 @@
-cicDisambiguate.cmi: 
-disambiguateChoices.cmi: 
 cicDisambiguate.cmo: cicDisambiguate.cmi 
 cicDisambiguate.cmx: cicDisambiguate.cmi 
 disambiguateChoices.cmo: disambiguateChoices.cmi 
diff --git a/helm/software/components/cic_exportation/.depend.opt b/helm/software/components/cic_exportation/.depend.opt
index 91be8d88d..288ea5f6c 100644
--- a/helm/software/components/cic_exportation/.depend.opt
+++ b/helm/software/components/cic_exportation/.depend.opt
@@ -1,3 +1,2 @@
-cicExportation.cmi: 
 cicExportation.cmo: cicExportation.cmi 
 cicExportation.cmx: cicExportation.cmi 
diff --git a/helm/software/components/cic_proof_checking/.depend.opt b/helm/software/components/cic_proof_checking/.depend.opt
index f8a16629e..5d83fd0f3 100644
--- a/helm/software/components/cic_proof_checking/.depend.opt
+++ b/helm/software/components/cic_proof_checking/.depend.opt
@@ -1,13 +1,3 @@
-cicLogger.cmi: 
-cicEnvironment.cmi: 
-cicPp.cmi: 
-cicUnivUtils.cmi: 
-cicSubstitution.cmi: 
-cicMiniReduction.cmi: 
-cicReduction.cmi: 
-cicTypeChecker.cmi: 
-freshNamesGenerator.cmi: 
-cicDischarge.cmi: 
 cicLogger.cmo: cicLogger.cmi 
 cicLogger.cmx: cicLogger.cmi 
 cicEnvironment.cmo: cicEnvironment.cmi 
diff --git a/helm/software/components/cic_unification/.depend.opt b/helm/software/components/cic_unification/.depend.opt
index 2e054f73d..a7b23ceb4 100644
--- a/helm/software/components/cic_unification/.depend.opt
+++ b/helm/software/components/cic_unification/.depend.opt
@@ -1,10 +1,3 @@
-cicMetaSubst.cmi: 
-cicMkImplicit.cmi: 
-termUtil.cmi: 
-coercGraph.cmi: 
-cicUnification.cmi: 
-cicReplace.cmi: 
-cicRefine.cmi: 
 cicMetaSubst.cmo: cicMetaSubst.cmi 
 cicMetaSubst.cmx: cicMetaSubst.cmi 
 cicMkImplicit.cmo: cicMkImplicit.cmi 
diff --git a/helm/software/components/content_pres/.depend.opt b/helm/software/components/content_pres/.depend.opt
index 8d74439eb..6dd0e78a1 100644
--- a/helm/software/components/content_pres/.depend.opt
+++ b/helm/software/components/content_pres/.depend.opt
@@ -1,9 +1,3 @@
-renderingAttrs.cmi: 
-cicNotationLexer.cmi: 
-cicNotationParser.cmi: 
-mpresentation.cmi: 
-box.cmi: 
-content2presMatcher.cmi: 
 termContentPres.cmi: cicNotationParser.cmi 
 boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi 
 cicNotationPres.cmi: mpresentation.cmi box.cmi 
diff --git a/helm/software/components/disambiguation/.depend.opt b/helm/software/components/disambiguation/.depend.opt
index 9fdbeeeaf..aba9ffea7 100644
--- a/helm/software/components/disambiguation/.depend.opt
+++ b/helm/software/components/disambiguation/.depend.opt
@@ -1,4 +1,3 @@
-disambiguateTypes.cmi: 
 disambiguate.cmi: disambiguateTypes.cmi 
 multiPassDisambiguator.cmi: disambiguateTypes.cmi disambiguate.cmi 
 disambiguateTypes.cmo: disambiguateTypes.cmi 
diff --git a/helm/software/components/extlib/.depend.opt b/helm/software/components/extlib/.depend.opt
index dcc6377a0..201cd0cba 100644
--- a/helm/software/components/extlib/.depend.opt
+++ b/helm/software/components/extlib/.depend.opt
@@ -1,13 +1,3 @@
-componentsConf.cmi: 
-hExtlib.cmi: 
-hMarshal.cmi: 
-patternMatcher.cmi: 
-hLog.cmi: 
-trie.cmi: 
-discrimination_tree.cmi: 
-hTopoSort.cmi: 
-refCounter.cmi: 
-graphvizPp.cmi: 
 componentsConf.cmo: componentsConf.cmi 
 componentsConf.cmx: componentsConf.cmi 
 hExtlib.cmo: hExtlib.cmi 
diff --git a/helm/software/components/getter/.depend.opt b/helm/software/components/getter/.depend.opt
index 64da37f13..554fb1ec7 100644
--- a/helm/software/components/getter/.depend.opt
+++ b/helm/software/components/getter/.depend.opt
@@ -1,13 +1,6 @@
-http_getter_wget.cmi: 
-http_getter_logger.cmi: 
-http_getter_misc.cmi: 
-http_getter_const.cmi: 
 http_getter_env.cmi: http_getter_types.cmx 
-http_getter_storage.cmi: 
 http_getter_common.cmi: http_getter_types.cmx 
 http_getter.cmi: http_getter_types.cmx 
-http_getter_types.cmo: 
-http_getter_types.cmx: 
 http_getter_wget.cmo: http_getter_types.cmx http_getter_wget.cmi 
 http_getter_wget.cmx: http_getter_types.cmx http_getter_wget.cmi 
 http_getter_logger.cmo: http_getter_logger.cmi 
diff --git a/helm/software/components/grafite/.depend.opt b/helm/software/components/grafite/.depend.opt
index e01d5bbfa..0f64ba789 100644
--- a/helm/software/components/grafite/.depend.opt
+++ b/helm/software/components/grafite/.depend.opt
@@ -1,7 +1,5 @@
 grafiteAstPp.cmi: grafiteAst.cmx 
 grafiteMarshal.cmi: grafiteAst.cmx 
-grafiteAst.cmo: 
-grafiteAst.cmx: 
 grafiteAstPp.cmo: grafiteAst.cmx grafiteAstPp.cmi 
 grafiteAstPp.cmx: grafiteAst.cmx grafiteAstPp.cmi 
 grafiteMarshal.cmo: grafiteAstPp.cmi grafiteAst.cmx grafiteMarshal.cmi 
diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 0cfdef148..7754102c6 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -57,6 +57,9 @@ type ntactic =
    | NChange of loc * npattern * CicNotationPt.term
    | NConstructor of loc * int option * CicNotationPt.term list
    | NCut of loc * CicNotationPt.term
+(* | NDiscriminate of loc * CicNotationPt.term
+   | NSubst of loc * CicNotationPt.term *)
+   | NDestruct of loc
    | NElim of loc * CicNotationPt.term * npattern  
    | NGeneralize of loc * npattern
    | NId of loc
@@ -71,6 +74,7 @@ type ntactic =
    | NBranch of loc
    | NShift of loc
    | NPos of loc * int list
+   | NPosbyname of loc * string
    | NWildcard of loc
    | NMerge of loc
    | NSkip of loc
@@ -197,7 +201,7 @@ type nmacro =
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)
-let magic = 30
+let magic = 33
 
 type ('term,'obj) command =
   | Index of loc * 'term option (* key *) * UriManager.uri (* value *)
@@ -220,6 +224,7 @@ type ('term,'obj) command =
 type ncommand =
   | UnificationHint of loc * CicNotationPt.term * int (* term, precedence *)
   | NObj of loc * CicNotationPt.term CicNotationPt.obj
+  | NDiscriminator of loc * CicNotationPt.term
   | NInverter of loc * string * CicNotationPt.term * bool list option * CicNotationPt.term option
   | NUnivConstraint of loc * NUri.uri * NUri.uri
   | NCopy of loc * string * NUri.uri * (NUri.uri * NUri.uri) list
diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 83f3a36b6..0db8efc1a 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -111,6 +111,9 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ 
       " with " ^ CicNotationPp.pp_term wwhat
   | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
+(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
+  | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
+  | NDestruct _ -> "ndestruct"
   | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
       assert false ^ " " ^ assert false
   | NId _ -> "nid"
@@ -125,6 +128,7 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NBranch _ -> "##["
   | NShift _ -> "##|"
   | NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
+  | NPosbyname (_, s) -> "##" ^ s ^ ":"
   | NWildcard _ -> "##*:"
   | NMerge _ -> "##]"
   | NFocus (_,l) -> 
@@ -371,6 +375,7 @@ let pp_coercion ~term_pp t do_composites arity saturations=
 let pp_ncommand = function
   | UnificationHint (_,t, n) -> 
       "unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+  | NDiscriminator (_,_)
   | NInverter (_,_,_,_,_)
   | NObj (_,_)
   | NUnivConstraint (_) -> "not supported"
diff --git a/helm/software/components/grafite_engine/.depend.opt b/helm/software/components/grafite_engine/.depend.opt
index 10236823a..a545f14e3 100644
--- a/helm/software/components/grafite_engine/.depend.opt
+++ b/helm/software/components/grafite_engine/.depend.opt
@@ -1,4 +1,3 @@
-grafiteTypes.cmi: 
 grafiteSync.cmi: grafiteTypes.cmi 
 nCicCoercDeclaration.cmi: grafiteTypes.cmi 
 grafiteEngine.cmi: grafiteTypes.cmi 
diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index fd8d776c1..248c02fa5 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -759,6 +759,9 @@ let eval_ng_tac tac =
      NTactics.constructor_tac 
        ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
   | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
+(*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
+  | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
+  | GrafiteAst.NDestruct _ -> NDestructTac.destruct_tac
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac 
@@ -775,6 +778,7 @@ let eval_ng_tac tac =
         ~what:(text,prefix_len,what) name
   | GrafiteAst.NMerge _ -> NTactics.merge_tac 
   | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
+  | GrafiteAst.NPosbyname (_,s) -> NTactics.case_tac s
   | GrafiteAst.NReduce (_loc, reduction, where) ->
       NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
@@ -991,6 +995,24 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
           [] ->
            eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
         | _ -> status,`New [])
+  | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) ->
+      if status#ng_mode <> `CommandMode then
+        raise (GrafiteTypes.Command_error "Not in command mode")
+      else
+        let status = status#set_ng_mode `ProofMode in
+        let metasenv,subst,status,indty =
+          GrafiteDisambiguate.disambiguate_nterm None status [] [] [] (text,prefix_len,indty) in
+        let indtyno, (_,_,tys,_,_) = match indty with
+            NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
+              indtyno, NCicEnvironment.get_checked_indtys r
+          | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
+        let it = List.nth tys indtyno in
+        let status,obj =  NDestructTac.mk_discriminator it status in
+        let _,_,menv,_,_ = obj in
+          (match menv with
+               [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+             | _ -> prerr_endline ("Discriminator: non empty metasenv");
+                    status, `New []) *)
   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
      if status#ng_mode <> `CommandMode then
       raise (GrafiteTypes.Command_error "Not in command mode")
diff --git a/helm/software/components/grafite_parser/.depend.opt b/helm/software/components/grafite_parser/.depend.opt
index 2766b04d0..97bf4d7c2 100644
--- a/helm/software/components/grafite_parser/.depend.opt
+++ b/helm/software/components/grafite_parser/.depend.opt
@@ -1,9 +1,4 @@
-dependenciesParser.cmi: 
-grafiteParser.cmi: 
-cicNotation2.cmi: 
-nEstatus.cmi: 
 grafiteDisambiguate.cmi: nEstatus.cmi 
-print_grammar.cmi: 
 dependenciesParser.cmo: dependenciesParser.cmi 
 dependenciesParser.cmx: dependenciesParser.cmi 
 grafiteParser.cmo: grafiteParser.cmi 
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 0fc42291d..2914a8906 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -257,6 +257,9 @@ EXTEND
         G.NConstructor (loc,
            (match num with None -> None | Some x -> Some (int_of_string x)),l)
     | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
+(*  | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
+    | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
+    | IDENT "ndestruct" -> G.NDestruct loc
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         G.NElim (loc, what, where)
     | IDENT "ngeneralize"; p=pattern_spec ->
@@ -566,6 +569,7 @@ EXTEND
       | SYMBOL "|" -> G.NShift loc
       | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> G.NPos (loc, i)
       | SYMBOL "*"; SYMBOL ":" -> G.NWildcard loc
+      | name = IDENT; SYMBOL ":" -> G.NPosbyname (loc, name)
       | SYMBOL "]" -> G.NMerge loc
       | SYMBOL ";" -> G.NSemicolon loc
       | SYMBOL "." -> G.NDot loc
@@ -803,6 +807,7 @@ EXTEND
         G.NObj (loc, N.Theorem (nflavour, name, N.Implicit `JustOne, Some body,`Regular))
     | IDENT "naxiom"; name = IDENT; SYMBOL ":"; typ = term ->
         G.NObj (loc, N.Theorem (`Axiom, name, typ, None, `Regular))
+    | IDENT "ndiscriminator" ; indty = tactic_term -> G.NDiscriminator (loc,indty)
     | IDENT "ninverter"; name = IDENT; IDENT "for" ; indty = tactic_term ;
       paramspec = OPT inverter_param_list ; 
       outsort = OPT [ SYMBOL ":" ; outsort = term -> outsort ] -> 
diff --git a/helm/software/components/hgdome/.depend.opt b/helm/software/components/hgdome/.depend.opt
index 072d9697a..bf9c09af7 100644
--- a/helm/software/components/hgdome/.depend.opt
+++ b/helm/software/components/hgdome/.depend.opt
@@ -1,5 +1,3 @@
-domMisc.cmi: 
-xml2Gdome.cmi: 
 domMisc.cmo: domMisc.cmi 
 domMisc.cmx: domMisc.cmi 
 xml2Gdome.cmo: xml2Gdome.cmi 
diff --git a/helm/software/components/hmysql/.depend.opt b/helm/software/components/hmysql/.depend.opt
index c2289bff2..602c901b8 100644
--- a/helm/software/components/hmysql/.depend.opt
+++ b/helm/software/components/hmysql/.depend.opt
@@ -1,7 +1,2 @@
-hSql.cmi: 
-hSqlite3.cmo: 
-hSqlite3.cmx: 
-hMysql.cmo: 
-hMysql.cmx: 
 hSql.cmo: hSqlite3.cmx hMysql.cmx hSql.cmi 
 hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi 
diff --git a/helm/software/components/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt
index 0fee4b18e..463d8a7bc 100644
--- a/helm/software/components/lexicon/.depend.opt
+++ b/helm/software/components/lexicon/.depend.opt
@@ -3,8 +3,6 @@ lexiconMarshal.cmi: lexiconAst.cmx
 cicNotation.cmi: lexiconAst.cmx 
 lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi 
 lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx 
-lexiconAst.cmo: 
-lexiconAst.cmx: 
 lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi 
 lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi 
 lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi 
diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt
index cfa1295ed..a9f24f814 100644
--- a/helm/software/components/library/.depend.opt
+++ b/helm/software/components/library/.depend.opt
@@ -1,13 +1,4 @@
-librarian.cmi: 
-libraryMisc.cmi: 
-libraryDb.cmi: 
-coercDb.cmi: 
 cicCoercion.cmi: coercDb.cmi 
-librarySync.cmi: 
-cicElim.cmi: 
-cicRecord.cmi: 
-cicFix.cmi: 
-libraryClean.cmi: 
 librarian.cmo: librarian.cmi 
 librarian.cmx: librarian.cmi 
 libraryMisc.cmo: libraryMisc.cmi 
diff --git a/helm/software/components/logger/.depend.opt b/helm/software/components/logger/.depend.opt
index dfb4400ff..28268d29e 100644
--- a/helm/software/components/logger/.depend.opt
+++ b/helm/software/components/logger/.depend.opt
@@ -1,3 +1,2 @@
-helmLogger.cmi: 
 helmLogger.cmo: helmLogger.cmi 
 helmLogger.cmx: helmLogger.cmi 
diff --git a/helm/software/components/metadata/.depend.opt b/helm/software/components/metadata/.depend.opt
index 78cd97a0d..492a34e3a 100644
--- a/helm/software/components/metadata/.depend.opt
+++ b/helm/software/components/metadata/.depend.opt
@@ -1,5 +1,3 @@
-sqlStatements.cmi: 
-metadataTypes.cmi: 
 metadataExtractor.cmi: metadataTypes.cmi 
 metadataPp.cmi: metadataTypes.cmi 
 metadataConstraints.cmi: metadataTypes.cmi 
diff --git a/helm/software/components/ng_cic_content/.depend.opt b/helm/software/components/ng_cic_content/.depend.opt
index 1316c8eab..b4e17fa99 100644
--- a/helm/software/components/ng_cic_content/.depend.opt
+++ b/helm/software/components/ng_cic_content/.depend.opt
@@ -1,5 +1,3 @@
-ncic2astMatcher.cmi: 
-nTermCicContent.cmi: 
 ncic2astMatcher.cmo: ncic2astMatcher.cmi 
 ncic2astMatcher.cmx: ncic2astMatcher.cmi 
 nTermCicContent.cmo: ncic2astMatcher.cmi nTermCicContent.cmi 
diff --git a/helm/software/components/ng_disambiguation/.depend.opt b/helm/software/components/ng_disambiguation/.depend.opt
index 2de54dc5e..6b4ef95c1 100644
--- a/helm/software/components/ng_disambiguation/.depend.opt
+++ b/helm/software/components/ng_disambiguation/.depend.opt
@@ -1,3 +1,2 @@
-nCicDisambiguate.cmi: 
 nCicDisambiguate.cmo: nCicDisambiguate.cmi 
 nCicDisambiguate.cmx: nCicDisambiguate.cmi 
diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend
index 9a4ae3fc1..4d6080d8a 100644
--- a/helm/software/components/ng_kernel/.depend
+++ b/helm/software/components/ng_kernel/.depend
@@ -1,4 +1,3 @@
-nUri.cmi: 
 nReference.cmi: nUri.cmi 
 nCicUtils.cmi: nCic.cmo 
 nCicSubstitution.cmi: nCic.cmo 
diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt
index d7c542af5..d4a4f8303 100644
--- a/helm/software/components/ng_kernel/.depend.opt
+++ b/helm/software/components/ng_kernel/.depend.opt
@@ -1,4 +1,3 @@
-nUri.cmi: 
 nReference.cmi: nUri.cmi 
 nCicUtils.cmi: nCic.cmx 
 nCicSubstitution.cmi: nCic.cmx 
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 3cd11c0f8..c57055365 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -59,3 +59,7 @@ val debruijn:
 val are_all_occurrences_positive: 
  subst:NCic.substitution ->
   NCic.context -> NUri.uri -> int -> int -> int -> int -> NCic.term -> bool
+
+val does_not_occur :
+    subst:NCic.substitution ->
+    ('a * NCic.context_entry) list -> int -> int -> NCic.term -> bool
diff --git a/helm/software/components/ng_library/.depend b/helm/software/components/ng_library/.depend
index e379b9fc6..5e568e6b3 100644
--- a/helm/software/components/ng_library/.depend
+++ b/helm/software/components/ng_library/.depend
@@ -1,6 +1,3 @@
-nCic2OCic.cmi: 
-oCic2NCic.cmi: 
-nCicLibrary.cmi: 
 nCic2OCic.cmo: nCic2OCic.cmi 
 nCic2OCic.cmx: nCic2OCic.cmi 
 oCic2NCic.cmo: oCic2NCic.cmi 
diff --git a/helm/software/components/ng_library/.depend.opt b/helm/software/components/ng_library/.depend.opt
index e379b9fc6..5e568e6b3 100644
--- a/helm/software/components/ng_library/.depend.opt
+++ b/helm/software/components/ng_library/.depend.opt
@@ -1,6 +1,3 @@
-nCic2OCic.cmi: 
-oCic2NCic.cmi: 
-nCicLibrary.cmi: 
 nCic2OCic.cmo: nCic2OCic.cmi 
 nCic2OCic.cmx: nCic2OCic.cmi 
 oCic2NCic.cmo: oCic2NCic.cmi 
diff --git a/helm/software/components/ng_paramodulation/.depend.opt b/helm/software/components/ng_paramodulation/.depend.opt
index 369ed6b69..3ace51014 100644
--- a/helm/software/components/ng_paramodulation/.depend.opt
+++ b/helm/software/components/ng_paramodulation/.depend.opt
@@ -1,4 +1,3 @@
-terms.cmi: 
 pp.cmi: terms.cmi 
 foSubst.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
@@ -11,7 +10,6 @@ paramod.cmi: terms.cmi orderings.cmi
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
 nCicProof.cmi: terms.cmi 
-nCicParamod.cmi: 
 terms.cmo: terms.cmi 
 terms.cmx: terms.cmi 
 pp.cmo: terms.cmi pp.cmi 
diff --git a/helm/software/components/ng_refiner/.depend.opt b/helm/software/components/ng_refiner/.depend.opt
index db7e52884..f30b906fd 100644
--- a/helm/software/components/ng_refiner/.depend.opt
+++ b/helm/software/components/ng_refiner/.depend.opt
@@ -1,6 +1,3 @@
-nDiscriminationTree.cmi: 
-nCicMetaSubst.cmi: 
-nCicUnifHint.cmi: 
 nCicCoercion.cmi: nCicUnifHint.cmi 
 nRstatus.cmi: nCicCoercion.cmi 
 nCicUnification.cmi: nRstatus.cmi 
diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 2e709a0af..ef100f742 100644
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,11 +1,8 @@
-nCicTacReduction.cmi: 
-nTacStatus.cmi: 
-nCicElim.cmi: 
 nTactics.cmi: nTacStatus.cmi 
-zipTree.cmi: 
-andOrTree.cmi: 
+andOrTree.cmi: zipTree.cmi 
 nAuto.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
+nDestructTac.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
 nCicTacReduction.cmx: nCicTacReduction.cmi 
 nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
@@ -18,7 +15,9 @@ zipTree.cmo: zipTree.cmi
 zipTree.cmx: zipTree.cmi 
 andOrTree.cmo: zipTree.cmi andOrTree.cmi 
 andOrTree.cmx: zipTree.cmx andOrTree.cmi 
-nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi nAuto.cmi 
-nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx nAuto.cmi 
+nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi nAuto.cmi 
+nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx nAuto.cmi 
 nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 
 nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi 
+nDestructTac.cmo: nTactics.cmi nTacStatus.cmi nDestructTac.cmi 
+nDestructTac.cmx: nTactics.cmx nTacStatus.cmx nDestructTac.cmi 
diff --git a/helm/software/components/ng_tactics/.depend.opt b/helm/software/components/ng_tactics/.depend.opt
index 2e709a0af..ef100f742 100644
--- a/helm/software/components/ng_tactics/.depend.opt
+++ b/helm/software/components/ng_tactics/.depend.opt
@@ -1,11 +1,8 @@
-nCicTacReduction.cmi: 
-nTacStatus.cmi: 
-nCicElim.cmi: 
 nTactics.cmi: nTacStatus.cmi 
-zipTree.cmi: 
-andOrTree.cmi: 
+andOrTree.cmi: zipTree.cmi 
 nAuto.cmi: nTacStatus.cmi 
 nInversion.cmi: nTacStatus.cmi 
+nDestructTac.cmi: nTacStatus.cmi 
 nCicTacReduction.cmo: nCicTacReduction.cmi 
 nCicTacReduction.cmx: nCicTacReduction.cmi 
 nTacStatus.cmo: nCicTacReduction.cmi nTacStatus.cmi 
@@ -18,7 +15,9 @@ zipTree.cmo: zipTree.cmi
 zipTree.cmx: zipTree.cmi 
 andOrTree.cmo: zipTree.cmi andOrTree.cmi 
 andOrTree.cmx: zipTree.cmx andOrTree.cmi 
-nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi nAuto.cmi 
-nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx nAuto.cmi 
+nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi nAuto.cmi 
+nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx nAuto.cmi 
 nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi 
 nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi 
+nDestructTac.cmo: nTactics.cmi nTacStatus.cmi nDestructTac.cmi 
+nDestructTac.cmx: nTactics.cmx nTacStatus.cmx nDestructTac.cmi 
diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile
index f05c75e94..6bb0ac3ee 100644
--- a/helm/software/components/ng_tactics/Makefile
+++ b/helm/software/components/ng_tactics/Makefile
@@ -8,7 +8,8 @@ INTERFACE_FILES = \
 	zipTree.mli \
 	andOrTree.mli \
 	nAuto.mli \
-	nInversion.mli
+	nInversion.mli \
+	nDestructTac.mli
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index b6013c272..b58eb5558 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -229,6 +229,10 @@ let get_goalty status g =
  with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_goalty")
 ;;
 
+let get_subst status =
+  let _,_,_,subst,_ = status#obj in subst
+;;
+
 let to_subst status i entry =
  let name,height,metasenv,subst,obj = status#obj in
  let metasenv = List.filter (fun j,_ -> j <> i) metasenv in
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index ec9f7738a..bf2370ec9 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -62,6 +62,7 @@ val saturate :
 val metas_of_term : #pstatus as 'status -> cic_term -> int list
 
 val get_goalty: #pstatus -> int -> cic_term
+val get_subst: #pstatus -> NCic.substitution
 val mk_meta: 
  #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
    [ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index d366c87d2..10fa168d4 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -52,7 +52,7 @@ let branch_tac status =
     | [] -> assert false
     | (g, t, k, tag) :: s ->
           match init_pos g with (* TODO *)
-          | [] | [ _ ] -> fail (lazy "too few goals to branch");
+          | [] | [ _ ] -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
   in
@@ -478,6 +478,8 @@ type indtyinfo = {
  }
 ;;
 
+let ref_of_indtyinfo iti = iti.reference;;
+
 let analyze_indty_tac ~what indtyref =
  distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index b8659c357..25baae97a 100644
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -48,6 +48,7 @@ val rewrite_tac:
    what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 
     's NTacStatus.tactic
 val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
+val clear_tac : string list -> 's NTacStatus.tactic
 val reduce_tac: 
       reduction:[ `Normalize of bool | `Whd of bool ] ->
       where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
@@ -61,3 +62,29 @@ val assert_tac:
 
 val constructor_tac : 
         ?num:int -> args:NTacStatus.tactic_term list -> 's NTacStatus.tactic
+
+val atomic_tac :
+    (((int * Continuationals.Stack.switch) list * 'a list * 'b list *
+      [> `NoTag ])
+     list NTacStatus.status ->
+     (< auto_cache : NCicLibrary.automation_cache;
+        coerc_db : NCicCoercion.db; dump : NCicLibrary.obj list;
+        lstatus : LexiconEngine.lexicon_status; obj : NCic.obj;
+        set_coerc_db : NCicCoercion.db -> 'c;
+        set_coercion_status : 'd. (#NCicCoercion.g_status as 'd) -> 'c;
+        set_uhint_db : NCicUnifHint.db -> 'c;
+        set_unifhint_status : 'e. (#NCicUnifHint.g_status as 'e) -> 'c;
+        timestamp : NCicLibrary.timestamp; uhint_db : NCicUnifHint.db; .. >
+      as 'c)) ->
+    (#NTacStatus.tac_status as 'f) -> 'f
+
+type indtyinfo 
+
+val ref_of_indtyinfo : indtyinfo -> NReference.reference
+
+val analyze_indty_tac :
+    what:NTacStatus.tactic_term ->
+    indtyinfo option ref -> (#NTacStatus.tac_status as 'a) -> 'a
+
+
+val find_in_context : 'a -> ('a * 'b) list -> int
diff --git a/helm/software/components/registry/.depend.opt b/helm/software/components/registry/.depend.opt
index 40c03891a..cf4f36b68 100644
--- a/helm/software/components/registry/.depend.opt
+++ b/helm/software/components/registry/.depend.opt
@@ -1,3 +1,2 @@
-helm_registry.cmi: 
 helm_registry.cmo: helm_registry.cmi 
 helm_registry.cmx: helm_registry.cmi 
diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend
index 25e67131f..f3c6a8bd1 100644
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,5 +1,2 @@
-utf8Macro.cmi: 
-utf8MacroTable.cmo: 
-utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
diff --git a/helm/software/components/syntax_extensions/.depend.opt b/helm/software/components/syntax_extensions/.depend.opt
index 3d7dfc21f..c0cd9c906 100644
--- a/helm/software/components/syntax_extensions/.depend.opt
+++ b/helm/software/components/syntax_extensions/.depend.opt
@@ -1,5 +1,2 @@
-utf8Macro.cmi: 
-utf8MacroTable.cmo: 
-utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmx utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
diff --git a/helm/software/components/tactics/.depend.opt b/helm/software/components/tactics/.depend.opt
index d9d6034a1..169fc76b0 100644
--- a/helm/software/components/tactics/.depend.opt
+++ b/helm/software/components/tactics/.depend.opt
@@ -1,19 +1,11 @@
-proofEngineTypes.cmi: 
 proofEngineHelpers.cmi: proofEngineTypes.cmi 
-proofEngineReduction.cmi: 
 continuationals.cmi: proofEngineTypes.cmi 
 tacticals.cmi: proofEngineTypes.cmi 
 reductionTactics.cmi: proofEngineTypes.cmi 
 proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
 primitiveTactics.cmi: proofEngineTypes.cmi 
-hashtbl_equiv.cmi: 
 metadataQuery.cmi: proofEngineTypes.cmi 
-universe.cmi: 
 autoTypes.cmi: proofEngineTypes.cmi 
-autoCache.cmi: 
-paramodulation/utils.cmi: 
-closeCoercionGraph.cmi: 
-paramodulation/subst.cmi: 
 paramodulation/equality.cmi: paramodulation/utils.cmi \
     paramodulation/subst.cmi 
 paramodulation/founif.cmi: paramodulation/subst.cmi 
@@ -35,13 +27,10 @@ equalityTactics.cmi: proofEngineTypes.cmi
 auto.cmi: proofEngineTypes.cmi automationCache.cmi 
 destructTactic.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
-inversion_principle.cmi: 
 ring.cmi: proofEngineTypes.cmi 
 setoids.cmi: proofEngineTypes.cmi 
-fourier.cmi: 
 fourierR.cmi: proofEngineTypes.cmi 
 fwdSimplTactic.cmi: proofEngineTypes.cmi 
-history.cmi: 
 statefulProofEngine.cmi: proofEngineTypes.cmi 
 tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi 
 declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi 
diff --git a/helm/software/components/thread/.depend.opt b/helm/software/components/thread/.depend.opt
index 6616a03d0..7759190c6 100644
--- a/helm/software/components/thread/.depend.opt
+++ b/helm/software/components/thread/.depend.opt
@@ -1,5 +1,3 @@
-threadSafe.cmi: 
-extThread.cmi: 
 threadSafe.cmo: threadSafe.cmi 
 threadSafe.cmx: threadSafe.cmi 
 extThread.cmo: extThread.cmi 
diff --git a/helm/software/components/tptp_grafite/.depend.opt b/helm/software/components/tptp_grafite/.depend.opt
index fb60fe8f2..c74300207 100644
--- a/helm/software/components/tptp_grafite/.depend.opt
+++ b/helm/software/components/tptp_grafite/.depend.opt
@@ -1,7 +1,4 @@
 parser.cmi: ast.cmx 
-tptp2grafite.cmi: 
-ast.cmo: 
-ast.cmx: 
 lexer.cmo: parser.cmi 
 lexer.cmx: parser.cmx 
 parser.cmo: ast.cmx parser.cmi 
diff --git a/helm/software/components/urimanager/.depend.opt b/helm/software/components/urimanager/.depend.opt
index 9cac9aa78..482148423 100644
--- a/helm/software/components/urimanager/.depend.opt
+++ b/helm/software/components/urimanager/.depend.opt
@@ -1,3 +1,2 @@
-uriManager.cmi: 
 uriManager.cmo: uriManager.cmi 
 uriManager.cmx: uriManager.cmi 
diff --git a/helm/software/components/whelp/.depend.opt b/helm/software/components/whelp/.depend.opt
index 65dc07955..39f37dfa9 100644
--- a/helm/software/components/whelp/.depend.opt
+++ b/helm/software/components/whelp/.depend.opt
@@ -1,5 +1,3 @@
-whelp.cmi: 
-fwdQueries.cmi: 
 whelp.cmo: whelp.cmi 
 whelp.cmx: whelp.cmi 
 fwdQueries.cmo: fwdQueries.cmi 
diff --git a/helm/software/components/xml/.depend.opt b/helm/software/components/xml/.depend.opt
index e7e7ffbd7..5ef59bdc9 100644
--- a/helm/software/components/xml/.depend.opt
+++ b/helm/software/components/xml/.depend.opt
@@ -1,5 +1,3 @@
-xml.cmi: 
-xmlPushParser.cmi: 
 xml.cmo: xml.cmi 
 xml.cmx: xml.cmi 
 xmlPushParser.cmo: xmlPushParser.cmi 
diff --git a/helm/software/components/xmldiff/.depend.opt b/helm/software/components/xmldiff/.depend.opt
index 65bd7b949..e2832de33 100644
--- a/helm/software/components/xmldiff/.depend.opt
+++ b/helm/software/components/xmldiff/.depend.opt
@@ -1,3 +1,2 @@
-xmlDiff.cmi: 
 xmlDiff.cmo: xmlDiff.cmi 
 xmlDiff.cmx: xmlDiff.cmi 
diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend
index c9a27fc56..9ebd03a64 100644
--- a/helm/software/matita/.depend
+++ b/helm/software/matita/.depend
@@ -1,7 +1,5 @@
 applyTransformation.cmo: applyTransformation.cmi 
 applyTransformation.cmx: applyTransformation.cmi 
-buildTimeConf.cmo: 
-buildTimeConf.cmx: 
 dump_moo.cmo: buildTimeConf.cmo 
 dump_moo.cmx: buildTimeConf.cmx 
 lablGraphviz.cmo: lablGraphviz.cmi 
@@ -26,8 +24,6 @@ matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
 matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi 
 matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi 
 matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi 
-matitaGeneratedGui.cmo: 
-matitaGeneratedGui.cmx: 
 matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \
     matitaGtkMisc.cmi 
 matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
@@ -72,21 +68,8 @@ predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi
 predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi 
 virtuals.cmo: virtuals.cmi 
 virtuals.cmx: virtuals.cmi 
-applyTransformation.cmi: 
-lablGraphviz.cmi: 
-matitaAutoGui.cmi: 
-matitaclean.cmi: 
-matitacLib.cmi: 
-matitadep.cmi: 
-matitaEngine.cmi: 
-matitaExcPp.cmi: 
 matitaGtkMisc.cmi: matitaGeneratedGui.cmo 
 matitaGui.cmi: matitaGuiTypes.cmi 
 matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo 
-matitaInit.cmi: 
 matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi 
-matitaMisc.cmi: 
 matitaScript.cmi: matitaTypes.cmi 
-matitaTypes.cmi: 
-predefined_virtuals.cmi: 
-virtuals.cmi: 
diff --git a/helm/software/matita/contribs/POPLmark/depends b/helm/software/matita/contribs/POPLmark/depends
index 02154bda1..7e7b8ae97 100644
--- a/helm/software/matita/contribs/POPLmark/depends
+++ b/helm/software/matita/contribs/POPLmark/depends
@@ -1,10 +1,12 @@
-Fsub/part1a_inversion.ma Fsub/defn.ma
 Fsub/part1a.ma Fsub/defn.ma
-Fsub/defn.ma Fsub/util.ma
 Fsub/util.ma list/in.ma list/list.ma logic/equality.ma nat/compare.ma
-Fsub/part1a_inversion2.ma Fsub/defn2.ma
-Fsub/defn2.ma Fsub/util.ma
+Fsub/defn.ma Fsub/util.ma
+Fsub/adeq.ma Fsub/part1a.ma
+Fsub/part1adb.ma Fsub/defndb.ma nat/le_arith.ma nat/lt_arith.ma
+Fsub/defndb.ma Fsub/util.ma nat/le_arith.ma nat/lt_arith.ma
 list/in.ma 
 list/list.ma 
 logic/equality.ma 
 nat/compare.ma 
+nat/le_arith.ma 
+nat/lt_arith.ma 
diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang
index 6a24b9aed..8b9577181 100644
--- a/helm/software/matita/matita.lang
+++ b/helm/software/matita/matita.lang
@@ -206,7 +206,8 @@
     <keyword>nchange</keyword>	    	 
     <keyword>nrewrite</keyword>	    	 
     <keyword>ncut</keyword>	    	 
-    <keyword>nlapply</keyword>	    	 
+    <keyword>nlapply</keyword>
+    <keyword>ndestruct</keyword> 
 </keyword-list>
 
   <keyword-list _name = "Tacticals" style = "Keyword" case-sensitive="TRUE">
diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index f188bf80f..49a03ff0f 100644
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -11,51 +11,34 @@
 (*        v         GNU General Public License Version 2                  *)
 (*                                                                        *)
 (**************************************************************************)
-(*
-include "nat/nat.ma".
-include "list/list.ma".
-
-inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
-| il_s : ∀n.T n → index_list T n n
-| il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
-
-lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
-                ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
-intros 5;elim i
-[destruct;apply il_s;apply f;assumption
-|apply il_c
- [apply f;rewrite > H;assumption
- |apply f1
-  [rewrite > H;reflexivity
-  |assumption]]]
-qed.
-
-definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝
-  λT0:Type.λT1:T0 → Type.
-  λa0,b0:T0.
-  λe0:a0 = b0.
-  λso:T1 a0.
-  eq_rect' ?? (λy,p.T1 y) so ? e0.
-  *)
 
 include "logic/equality.ma".
+
+(* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
+               ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
+#T;#a;#b;#e;#P;#H;
+nrewrite < e;*)
+
+ndefinition R0 ≝ λT:Type[0].λt:T.t.
   
 ndefinition R1 ≝ eq_rect_Type0.
+
 ndefinition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
   ∀a1:T1 a0 (refl ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+  ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:R1 ? a0 ? a1 ? e0 = b1. (* eccezine se tolgo a0 *)
-  ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1.
-#T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H;
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
+  T2 b0 e0 b1 e1.
+#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
 napply (eq_rect_Type0 ????? e1);
 napply (R1 ?? ? ?? e0);
-napply H;
+napply a2;
 nqed.
 
 ndefinition R3 :
@@ -63,19 +46,112 @@ ndefinition R3 :
   ∀a0:T0.
   ∀T1:∀x0:T0. a0=x0 → Type[0].
   ∀a1:T1 a0 (refl ? a0).
-  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ? a0 ? a1 ? p0 = x1 → Type[0].
+  ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
-  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ? a0 ? a1 ? p0 = x1.
-      ∀x2:T2 x0 p0 x1 p1.R2 ? a0 ? a1 ? ? p0 ? p1 a2 = x2 → Type[0].
+  ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+      ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+  ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
-  ∀e1:R1 ? a0 ? a1 ? e0 = b1.
+  ∀e1:R1 ?? T1 a1 ? e0 = b1.
   ∀b2: T2 b0 e0 b1 e1.
-  ∀e2:R2 ? a0 ? a1 ? ? e0 ? e1 a2 = b2.
-  ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2.
-#T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H;
+  ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+  T3 b0 e0 b1 e1 b2 e2.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
 napply (eq_rect_Type0 ????? e2);
-napply (R2 ?? ? ??? e0 ? e1);
-napply H;
-nqed.
\ No newline at end of file
+napply (R2 ?? ? ???? e0 ? e1);
+napply a3;
+nqed.
+
+(* include "nat/nat.ma".
+
+ninductive nlist : nat → Type[0] ≝
+| nnil : nlist O
+| ncons : ∀n:nat.nat → nlist n → nlist (S n).
+
+ninductive wrapper : Type[0] ≝
+| kw1 : ∀x.∀y:nlist x.wrapper
+| kw2 : ∀x.∀y:nlist x.wrapper.
+
+nlemma fie : ∀a,b,c,d.∀e:eq ? (kw1 a b) (kw1 c d). 
+             ∀P:(∀x1.∀x2:nlist x1. ∀y1.∀y2:nlist y1.eq ? (kw1 x1 x2) (kw1 y1 y2) → Prop). 
+             P a b a b (refl ??) → P a b c d e.
+#a;#b;#c;#d;#e;#P;#HP;
+ndiscriminate e;#e0;
+nsubst e0;#e1;
+nsubst e1;#E;
+(* nsubst E; purtroppo al momento funziona solo nel verso sbagliato *)
+nrewrite > E;
+napply HP;
+nqed.*) 
+
+(***************)
+
+ninductive I1 : Type[0] ≝
+| k1 : I1.
+
+ninductive I2 : I1 → Type[0] ≝
+| k2 : ∀x.I2 x.
+
+ninductive I3 : ∀x:I1.I2 x → Type[0] ≝
+| k3 : ∀x,y.I3 x y.
+
+ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
+| k4 : ∀x,y.∀z:I3 x y.I4 x y z.
+
+(*alias id "eq" = "cic:/matita/ng/logic/equality/eq.ind(1,0,2)".
+alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".*)
+
+ndefinition R4 :
+  ∀T0:Type[0].
+  ∀a0:T0.
+  ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+  ∀a1:T1 a0 (refl T0 a0).
+  ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+  ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
+  ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+  ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2). 
+  ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+      ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+      ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. 
+      Type[0].
+  ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+      a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2) 
+      a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) 
+                   a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+                   a3).
+  ∀b0:T0.
+  ∀e0:eq (T0 …) a0 b0.
+  ∀b1: T1 b0 e0.
+  ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+  ∀b2: T2 b0 e0 b1 e1.
+  ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+  ∀b3: T3 b0 e0 b1 e1 b2 e2.
+  ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+  T4 b0 e0 b1 e1 b2 e2 b3 e3.
+#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
+napply (eq_rect_Type0 ????? e3);
+napply (R3 ????????? e0 ? e1 ? e2);
+napply a4;
+nqed.
+
+
+ninductive II : Type[0] ≝
+| kII1 : ∀x,y,z.∀w:I4 x y z.II
+| kII2 : ∀x,y,z.∀w:I4 x y z.II.
+
+(* nlemma foo : ∀a,b,c,d,e,f,g,h. kII1 a b c d = kII2 e f g h → True.
+#a;#b;#c;#d;#e;#f;#g;#h;#H;
+ndiscriminate H;
+nqed. *)
+
+nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h.
+              ∀P:(∀a,b,c,d.kII1 a b c d = kII1 e f g h → Prop).
+              P e f g h (refl ??) → P a b c d Heq.
+#a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP;
+ndestruct;
+napply HP;
+nqed.
diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 715423143..b92f92f66 100644
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -28,6 +28,11 @@ nlemma eq_rect_CProp0_r:
  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
 nqed.
 
+nlemma eq_ind_r :
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
+nqed.
+
 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
 
 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma
index 8a44b8300..d9db8c39f 100644
--- a/helm/software/matita/nlibrary/logic/pts.ma
+++ b/helm/software/matita/nlibrary/logic/pts.ma
@@ -15,3 +15,4 @@
 universe constraint Type[0] < Type[1].
 universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
diff --git a/helm/software/matita/tests/destruct_bb.ma b/helm/software/matita/tests/destruct_bb.ma
index 494d5805a..382620e34 100644
--- a/helm/software/matita/tests/destruct_bb.ma
+++ b/helm/software/matita/tests/destruct_bb.ma
@@ -79,7 +79,7 @@ definition R2 :
   ∀b1: T1 b0 e0.
   ∀e1:R1 ??? a1 ? e0 = b1.
   T2 b0 e0 b1 e1.
-intros 9;intro e1;
+intros (T0 a0 T1 a1 T2 a2);
 apply (eq_rect' ????? e1);
 apply (R1 ?? ? ?? e0);
 simplify;assumption;
@@ -94,14 +94,15 @@ definition R3 :
   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
       ∀x2:T2 x0 p0 x1 p1.R2 T0 a0 T1 a1 T2 a2 ? p0 ? p1 = x2→ Type.
+  ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
   ∀b0:T0.
   ∀e0:a0 = b0.
   ∀b1: T1 b0 e0.
   ∀e1:R1 ??? a1 ? e0 = b1.
   ∀b2: T2 b0 e0 b1 e1.
   ∀e2:R2 T0 a0 T1 a1 T2 a2 ? e0 ? e1 = b2.
-  ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2.      
-intros 12;intros 2 (e2 H);
+  T3 b0 e0 b1 e1 b2 e2.       
+intros (T0 a0 T1 a1 T2 a2 T3 a3);
 apply (eq_rect' ????? e2);
 apply (R2 ?? ? ???? e0 ? e1);
 simplify;assumption;
@@ -194,16 +195,91 @@ inductive I2 : ∀n:nat.I1 n → Type ≝
 inductive I3 : Type ≝
 | kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
 
-definition I3d: I3 → I3 → Type ≝ 
-λx,y.match x with
+(* lemma idfof : (∀t1,t2,t3,u1,u2,u3.((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.
+       λy3:I2 y1 y2.λp3:R2 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 (λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1 =y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t3 y1 p1 y2 p2 =y3.
+                    kI3 y1 y2 y3 =kI3 u1 u2 u3)
+t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)
+   t3 (refl_eq ((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)) t3)
+   )
+    → True).
+simplify; *)
+
+definition I3d : ∀x,y:I3.x = y → Type ≝
+λx,y.match x return (λx:I3.x = y → Type) with
+[ kI3 x1 x2 x3 ⇒ match y return (λy:I3.kI3 x1 x2 x3 = y → Type) with
+  [ kI3 y1 y2 y3 ⇒ 
+    λe:kI3 x1 x2 x3 = kI3 y1 y2 y3.
+       ∀P:Prop.(∀e1: x1 = y1.
+                ∀e2: R1 ?? (λz1,p1.I1 z1) ?? e1 = y2.
+                ∀e3: R2 ???? (λz1,p1,z2,p2.I2 z1 z2) x3 ? e1 ? e2 = y3. 
+                R3 ?????? 
+                (λz1,p1,z2,p2,z3,p3.
+                  eq ? (kI3 z1 z2 z3) (kI3 y1 y2 y3)) e y1 e1 y2 e2 y3 e3
+                = refl_eq ? (kI3 y1 y2 y3)
+                → P) → P]].
+
+definition I3d : ∀x,y:I3.x=y → Type.
+intros 2;cases x;cases y;intro;
+apply (∀P:Prop.(∀e1: x1 = x3.
+                ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = x4.
+                ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) i ? e1 ? e2 = i1. 
+                R3 ?????? 
+                (λy1,p1,y2,p2,y3,p3.
+                  eq ? (kI3 y1 y2 y3) (kI3 x3 x4 i1)) H x3 e1 x4 e2 i1 e3
+                = refl_eq ? (kI3 x3 x4 i1)
+                → P) → P);
+qed.
+
+(* definition I3d : ∀x,y:nat. x = y → Type ≝
+λx,y.
+match x 
+ return (λx.x = y → Type)
+ with
+[ O ⇒ match y return (λy.O = y → Type) with
+  [ O ⇒ λe:O = O.∀P.P → P
+  | S q ⇒ λe: O = S q. ∀P.P]
+| S p ⇒ match y return (λy.S p = y → Type) with
+  [ O ⇒ λe:S p = O.∀P.P
+  | S q ⇒ λe: S p = S q. ∀P.(p = q → P) → P]]. 
+
+definition I3d: 
+  ∀x,y:I3. x = y → Type 
+  ≝ 
+λx,y. 
+match x with
+[ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
+  [ kI3 u1 u2 u3 ⇒ λe:kI3 t1 t2 t3 = kI3 u1 u2 u3.∀P:Type.
+    (∀e1: t1 = u1.
+     ∀e2: R1 nat t1 (λy1:nat.λp1:y1 = u1.I1 y1) t2 ? e1 = u2.
+     ∀e3: R2 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3. 
+     (* ∀e:  kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
+     R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 
+        (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) e u1 e1 u2 e2 u3 e3 = refl_eq I3 (kI3 u1 u2 u3)
+     → P)
+    → P]].
+
+definition I3d: 
+  ∀x,y:I3.
+    (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+      match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]) → Type 
+  ≝ 
+λx,y.λe:
+   (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
+      match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]). 
+match x with
 [ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
   [ kI3 u1 u2 u3 ⇒ ∀P:Type.
     (∀e1: t1 = u1.
      ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = u2.
-     ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) ? e1 ? e2 t3 = u3.P) → P]].
-
-lemma I3nc : ∀a,b.a = b → I3d a b.
-intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity;
+     ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3. 
+     (* ∀e:  kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
+     R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 
+        (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) (e (kI3 t1 t2 t3) (kI3 u1 u2 u3)) u1 e1 u2 e2 u3 e3 = refl_eq ? (kI3 u1 u2 u3)
+     → P)
+    → P]].*)
+     
+lemma I3nc : ∀a,b.∀e:a = b. I3d a b e.
+intros;apply (R1 ????? e);elim a;whd;intros;apply H;reflexivity;
 qed.
 
 (*lemma R1_r : ΠA:Type.Πx:A.ΠP:Πy:A.y=x→Type.P x (refl_eq A x)→Πy:A.Πp:y=x.P y p.
@@ -231,17 +307,25 @@ apply (R1_r ?? ? ?? e0);
 simplify;assumption;
 qed.*)
 
-definition I3prova : ∀a,b,c,d,e,f.kI3 a b c = kI3 d e f → ∃P.P d e f.
-intros;apply (I3nc ?? H);clear H;
+definition I3prova : ∀a,b,c,d,e,f.∀Heq:kI3 a b c = kI3 d e f.
+  ∀P:? → ? → ? → ? → Prop.
+  P d e f Heq → 
+  P a b c (refl_eq ??).
+intros;apply (I3nc ?? Heq);
 simplify;intro;
+generalize in match H as H;generalize in match Heq as Heq;
 generalize in match f as f;generalize in match e as e;
-generalize in match c as c;generalize in match b as b;
-clear f e c b;
+clear H Heq f e;
 apply (R1 ????? e1);intros 5;simplify in e2;
-generalize in match f as f;generalize in match c as c;
-clear f c;
-apply (R1 ????? e2);intros;simplify in H;
-elim daemon;
+generalize in match H as H;generalize in match Heq as Heq;
+generalize in match f as f;
+clear H Heq f;
+apply (R1 ????? e2);intros 4;simplify in e3;
+generalize in match H as H;generalize in match Heq as Heq;
+clear H Heq;
+apply (R1 ????? e3);intros;simplify in H1;
+apply (R1 ????? H1);
+assumption;
 qed.