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.
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.