theory Generic_Context imports Context_Notation begin locale "context" = context_notation + assumes compose_context_iff [simp]: "⋀(c :: 'c) c' (t :: 't). (c ∘⇩c c')⟨t⟩ = c⟨c'⟨t⟩⟩" and apply_hole [simp]: "⋀t. □⟨t⟩ = t" and apply_context_eq: "⋀c t t'. c⟨t⟩ = c⟨t'⟩ ⟹ t = t'" end