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)