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