Наблюдательное Равенство из Эпиграммы 2 кажется интенсиональным равенством (как у Coq и Agda), но оно также поддерживает расширяемость функций. В этом смысле кажется, что наблюдаемое равенство лучше во всех отношениях, чем интенсиональное равенство в теории типов. офф задействованы?