# Descind-laws


fx.experimental.desc-interp.descind-laws: kernel-level laws derived via `descInd kontQueueApp` at the indexed slice. Hosts qAppKernel (kernel-resident transposition of trampoline.qApp) and qAppIdLaw (qApp qIdentity x ≡ pure x as a kernel conv-witness).

## `qAppIdLaw`

_qAppIdLaw : Π(X:U). Π(x:X). bootEq (μ freeFx X) (qAppKernel (X,X) (qIdentity X) x) (pureCon X x). The Identity-collapse law as a kernel conv-witness; the proof is `bootRefl`, justified by descInd-on-descCon β through the Identity step body. Demonstrates that the indexed inductive hypothesis is operationally usable — the lemma's well-typedness depends essentially on `descInd kontQueueApp` projecting `fst_(i)` / `snd_(i)`._

```
qAppIdLaw : Π(X:U). Π(x:X). bootEq (μ freeFx X) (qAppKernel (X,X) (qIdentity X) x) (pureCon X x)
```

## `qAppIdLawTy`

_qAppIdLawTy Eff Resp: Π-type generated for the qApp identity law at one effect signature._

## `qAppKernel`

_qAppKernel Eff Resp i q x — kernel-resident `qApp` defined via `descInd kontQueueApp`. Identity branch returns `pureCon X x` (X = fst_(i) = snd_(i) forced by index); Leaf branch returns `fn x`; Node branch returns `bind (ih_l x) ih_r` cashing in both indexed IHs at (X,M) and (M,A). Mirrors `trampoline.qApp` but at the kernel layer._

```
qAppKernel : Hoas U -> Hoas (U -> U) -> Hoas U² -> Hoas (μI U² kontQueueApp i) -> Hoas (fst_(i)) -> Hoas (μ freeFxApp Eff Resp (snd_(i)) tt)
```