<p>I guess I don't really care about ssreflect for its own sake... what I really want is to understand enough to figure out how the mathcomp ppl can write their proofs without going insane. </p><p>Sadly I can't read even code that looks like [^=>/14<$//= or whatever</p>
