(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LOGIC/NTrack/defs".
+
(* NORMAL PROOF TREE TRACKS
*)
-include "datatypes/Proof.ma".
include "Insert/defs.ma".
-
+(*
inductive NTrack: Context \to Proof \to Sequent \to Prop \def
| ntrack_proj: \forall P,Q,S,i. Insert S i P Q \to NTrack Q (lref i) S
| ntrack_posr: \forall P,h.
Insert (pair A B) i P Q \to
NTrack P (impi p q r) (pair (impl a b) D)
.
+*)