Исключая SUBST доказательства равенства

Question

Я пытаюсь предст мод-п счетчиков в разрезе интервала [0, ..., n-1] на две части:

data Counter : ℕ → Set where 
    cut : (i j : ℕ) → Counter (suc (i + j)) 

Использование этого определения двух важнейших операций является прямым (некоторые доказательства опущены для краткости):

_+1 : ∀ {n} → Counter n → Counter n 
cut i zero +1 = subst Counter {!!} (cut zero i) 
cut i (suc j) +1 = subst Counter {!!} (cut (suc i) j) 

_-1 : ∀ {n} → Counter n → Counter n 
cut zero j -1 = subst Counter {!!} (cut j zero) 
cut (suc i) j -1 = subst Counter {!!} (cut i (suc j)) 

проблема возникает при попытке доказать, что +1 и -1 обратны. Я постоянно работаю в ситуацию, когда мне нужен выпрямитель для этих subst s введен, то есть что-то вроде

subst-elim : {A : Set} → {B : A → Set} → {x x′ : A} → {x=x′ : x ≡ x′} → {y : B x} → subst B x=x′ y ≡ y 
subst-elim {A} {B} {x} {.x} {refl} = refl 

, но это оказывается (несколько) попрошайничество вопроса: не принимается типа проверка, потому что subst B x=x' y : B x' и y : B x ...

Answer 1

Вы можете указать тип вашего суб-выключения, если вы используете Relation.Binary.HeterogeneousEquality из stdlib. Тем не менее, я бы, вероятно, просто совпадал с шаблоном на конечном доказательстве x ≡ x 'в выражении with или rewrite, поэтому вам не нужно делать явный выпрямитель и, следовательно, не печатать проблему.