+ (*
+ * A predicate singling out structural rules, initial sequents,
+ * and cut rules.
+ *
+ * Proofs using only structural rules cannot add or remove
+ * judgments - their hypothesis and conclusion judgment-trees will
+ * differ only in "parenthesization" and the presence/absence of
+ * empty leaves. This means that a proof involving only
+ * structural rules, cut, and initial sequents can ADD new
+ * non-empty judgment-leaves only via snd_initial, and can only
+ * REMOVE non-empty judgment-leaves only via snd_cut. Since the
+ * initial sequent is a left and right identity for cut, and cut
+ * is associative, any two proofs (with the same hypotheses and
+ * conclusions) using only structural rules, cut, and initial
+ * sequents are logically indistinguishable - their differences
+ * are logically insignificant.
+ *
+ * Note that it is important that nd_weak and nd_copy aren't
+ * considered to be "structural".
+ *)
+ Inductive SequentND_Inert : forall h c, h/⋯⋯/c -> Prop :=
+ | snd_inert_initial : forall a, SequentND_Inert _ _ (snd_initial a)
+ | snd_inert_cut : forall a b c, SequentND_Inert _ _ (snd_cut a b c)
+ | snd_inert_structural: forall a b f, Structural f -> SequentND_Inert a b f
+ .
+
+ (* An ND_Relation for a sequent deduction should not distinguish between two proofs having the same hypotheses and conclusions
+ * if those proofs use only initial sequents, cut, and structural rules (see comment above) *)
+ Class SequentND_Relation :=
+ { sndr_ndr := ndr
+ ; sndr_inert : forall a b (f g:a/⋯⋯/b),
+ NDPredicateClosure SequentND_Inert f ->
+ NDPredicateClosure SequentND_Inert g ->
+ ndr_eqv f g }.
+
+ End SequentND.
+
+ (* Deductions on sequents whose antecedent is a tree of propositions (i.e. a context) *)
+ Section ContextND.
+ Context {P:Type}{sequent:Tree ??P -> Tree ??P -> Judgment}.
+ Context {snd:SequentND(sequent:=sequent)}.