-- ≡-elim: eliminating a variable AND the equation that pins it.
--
-- `≡-elim p x w` takes a variable x and a hypothesis w proving x ≡ t
-- (or t ≡ x) for a t standing outside x's own entry, and elaborates p
-- where BOTH are gone: every hypothesis between and after them is
-- specialised at t, as is the goal. No motive is written — t is read
-- off w's type, and substituting it for x IS the motive.
--
-- Core/equality.nova's combinators say what this is NOT. Reflection
-- already makes x ≐ t judgemental wherever w is in scope, so transport
-- is the identity and cong is one ⋆; ≡-elim adds no power. What it
-- changes is the CONTEXT: the goal, and every hypothesis, restated at t
-- with the variable removed — the difference between reasoning about x
-- under an equation and reasoning about t with nothing left to carry.
import Natural (+)
pinned : (x : ℕ) (w : x ≡ Z) → x + x ≡ x using (Natural.plusZeroId)
pinned = λx w. ≡-elim ⋆ x w
-- the orientation is read off w's type: either side may be the
-- variable, and the rule is the same
pinnedFlipped : (x : ℕ) (w : Z ≡ x) → x + x ≡ x using (Natural.plusZeroId)
pinnedFlipped = λx w. ≡-elim ⋆ x w
-- a hypothesis standing BETWEEN the variable and the equation is
-- specialised with it, so inside, h is already the fact the goal wants
between : (x : ℕ) (h : x + x ≡ x) (w : x ≡ Z) → Z + Z ≡ Z
between = λx h w. ≡-elim h x w
-- and one standing AFTER the equation, likewise
after : (x : ℕ) (w : x ≡ Z) (h : x + x ≡ x) → Z + Z ≡ Z
after = λx w h. ≡-elim h x w
-- the eliminated variable's type need not be 𝕌-SMALL: the reflexivity
-- proof standing in for w is minted at the site, at whatever type the
-- variable had, so a variable ranging over 𝕌 eliminates like any other
atLarge : (x : 𝕌) (h : x) (w : x ≡ ℕ) → ℕ
atLarge = λx h w. ≡-elim h x w
-- the goal may name the eliminated PROOF, not just the variable:
-- [refl/w] puts that minted reference where w stood, and the site
-- converts back through the irrelevance equation
proofNamed : (x : ℕ) (w : x ≡ Z) → w ≡ w
proofNamed = λx w. ≡-elim ⋆ x w
-- t is any term standing outside the variable's own entry, not just a
-- constant: here it names an earlier hypothesis
atTerm : (n x : ℕ) (h : x + x ≡ x) (w : x ≡ n + n) → n + n + (n + n) ≡ n + n
atTerm = λn x h w. ≡-elim h x w
-- THE SLIDE: the equation's other side may name entries standing
-- AFTER the eliminated variable. A context is a telescope, so the
-- variable changes places with them — each exchange licensed by the
-- crossed entry not mentioning it — until that side stands in its
-- prefix. Here n is bound after x, and x slides past it
slid : (x n : ℕ) (h : x + x ≡ x) (w : x ≡ n + n) → n + n + (n + n) ≡ n + n
slid = λx n h w. ≡-elim h x w