- dd: Type[0]; (* denotations domain *)
- sq: relation2 dd dd; (* structural equivalence *)
- sv: nat → dd; (* sort evaluation *)
- ap: dd → dd → dd; (* application *)
- ti: (nat → dd) → (nat → dd) → term → dd (* term interperpretation *)
+(* Note: denotations domain *)
+ dd: Type[0];
+(* Note: structural equivalence *)
+ sq: relation2 dd dd;
+(* Note: sort evaluation *)
+ sv: nat → dd;
+(* Note: conjunction *)
+ co: bool → dd → dd → dd;
+(* Note: application *)
+ ap: dd → dd → dd;
+(* Note: term interperpretation *)
+ ti: (nat → dd) → (nat → dd) → term → dd