Skip to main content
7 votes

Policies on introducing free variables when rewriting?

If I understand correctly, what you are talking about is treated using existential variables in Coq. These are variables but on the "meta" level, meaning that they stand for a term yet-to-be-...
Meven Lennon-Bertrand's user avatar
3 votes

Policies on introducing free variables when rewriting?

In Metamath, the MMJ2 proof assistant introduces work variables, which names are constructed with a & prefix, a letter giving the type code of the variable, ...
Thierry Arnoux's user avatar
2 votes
Accepted

Higher Observational Type Theory: variables becoming free in reduction rules

I would guess the issue comes from the $\Delta$ you assumed was missing. As far as I can tell, when living over a general telescope, already $$ Id_{Δ.(Π (x : A) B)}^δ(f, g) ≡ \Pi (u, v : A). \Pi(p: ...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible