Denotation Properties

Extensionality, irrelevance, and structural properties of denote.

• denote_ext — extensionality: denotation depends only on used ops, fvars, and bvars
• denote_irrel_of_lcAt — closed expressions are independent of the bvar valuation
• denote_replaceMetadata — denotation is invariant under metadata replacement
• denoteArgs_eq_of_denote_eq / denoteArgs_eq_implies_denote_eq — pointwise ↔ aggregate argument equality

denoteConst properties

Denotation irrelevance for locally closed expressions

Collecting ops and bvar indices from an expression

Extensionality for denote

Metadata Doesn't Affect Typing or Denotations

fvars_annotated_by lemmas