// You don't need to follow the structure suggested here to receive full
// credit, but these ideas could help you get unstuck on some parts of the
// assignment.

// We found it useful to define the following:

datatype Option<T> = None | Some(value: T) // from Defs
type Tree // from the template

ghost function BlackHeight(s: Tree): Option<nat>
// Returns None if the tree is not well-formed in terms of black height.
// Otherwise returns the numeric height.

// Then Valid can be defined recursively using BlackHeight, Elements, and
// otherwise just built-in constructs.  With our definition, lemmas
// EmptyCorrect and MemberCorrect verify automatically.

// InsertCorrect is more work.  You might be tempted to prove a general
// inductive lemma about Ins, but we found it worked best to write InsertCorrect
// inductively, where the only lemma we proved about Ins concerns its effect on
// black height, specifically applying tight lower and upper bounds for the new
// black height in terms of the old.

// Finally, on the proof of balance: we proved a key lemma bounding minimum and
// maximum tree depths with linear expressions over black height. You probably
// want to take root color into account, to tweak the tightness of a bound.
// Our solution uses the fact that we can assign a slightly tighter depth
// upper bound when the root is black.  (And it's only *slightly* tighter;
// difference of one!)