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
• typeCheck_replaceMetadata1 / HasTypeA_replaceMetadata1 / denote_replaceMetadata1 — typing and denotation are invariant under root-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

Replacing only the root metadata

fvars_annotated_by lemmas