[thomaskwaring]

Add some constructions and results moving hypotheses between the set of axioms and context. Also clean up some naming including loose mentions of Theory which we have renamed.

[thomaskwaring]

@ctchou thanks for taking a look. i agree that the long _root_.<blah> are very ugly, the reason they're there is for dot notation: eg if h : DerivableIn (ND T) ... then i can write h.weak — do you think that's a good enough justification? the iff theorems aren't in the namespace bc for them the dot notation is useless

[ctchou]

Note that all the _root_.Cslib.Logic. prefixes are on theorem names. I think there is less a justification for the dot-notation in proofs. Alternatively, I wonder if it is possible to reorder the theorems so that all the theorems about InferenceSystem can be placed together in their own namespace scope.

I don't think the namespace of a theorem should not be determined by whether you want to use the dot-notation, but by conceptual consistency.

[chenson2018]

I think there is less a justification for the dot-notation in proofs.

I'm not reading this PR closely, just chiming in that dot notation can be extremely helpful for proofs as well.

[thomaskwaring]

i disagree about the usefulness of dot notation in proofs, but i hadn't thought about the fact that there might be other proof systems which want to use DerivableIn.weaken, and it doesn't make sense to pollute that namespace with natural deduction results.

in any case i've removed those _root_ namespaced declarations — i'm not totally sure the new names are right, but they're certainly better this way, thanks!

(if you decide to approve this, could you hold off merging until @jessealama has a chance to take a look, i want to make sure i'm stating / proving things that are usefully for his work)

[ctchou]

LGTM.