move funext_from_interval to IntervalImpliesFunext, not exported by HoTT

Because he's just writing out explicit proof terms :-)