@AntonTrunov во 2ой лекции введение равенства мне кажется будет даваться всем студентам тяжело, потому что вряд ли они сталкивались с завтипами. Внесет путаницу, что есть тип, а что конструкция.
Ага, спасибо. Надо подумать как ещё проще это объяснить. Но именно в этом и идея, чтобы построить всё «с нуля», чтобы можно было леммы формулировать