move funext_from_interval to IntervalImpliesFunext, not exported by HoTT
Merge pull request #523 from mikeshulman/interval

move funext_from_interval to IntervalImpliesFunext, not exported by HoTT