Стандартная библиотека Coq имеет два типа единиц измерения.Один True набирается в Prop и имеет один конструктор I : True.Другой unit набирается в Set и имеет один конструктор tt : unit.Интересно, каково происхождение имен I и tt.
True
Prop
I : True
unit
Set
tt : unit
I
tt