||2|| can replace I in the proof of funext, close #647
Merge pull request #648 from mikeshulman/truncbool

||2|| can replace I in the proof of funext, close #647