I can't find the function congruence lemma for Pure anywhere:

```
lemma pure_cong: "f ≡ g ⟹ x ≡ y ⟹ f x ≡ g y" by simp
```

with sorts, just for clarification:

```
⟦?f::?'a::{} ⇒ ?'b::{} ≡ ?g::?'a::{} ⇒ ?'b::{}; ?x::?'a::{} ≡ ?y::?'a::{}⟧ ⟹ ?f ?x ≡ ?g ?y
```

Is it really not stated as such anywhere in Pure or am I missing the obvious?

As far as I know this an axiom about Pure equality(Pure.combination). It could be retrieved from ML

```
Thm.axiom @{theory} "Pure.combination"
```

I do not know why this is not made available like other ones(e.g. Pure.reflexive)

Ahhh, combination and not cong! :light_bulb: Thank you :)

Last updated: Oct 13 2024 at 01:36 UTC