More indentation nonsense
Minor tweaks to eq-reflection
Generalize eq-reflect to proof search