<div dir="ltr"><div>```<br>removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) (_←⊂ {lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) | (drepl=>repl+ {frll = frll} ind lind)<br>... | g | r = {!!} <br><br>```<br></div>case splitting creates this:<br><div><div><br>```<br>removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) (_←⊂ {lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) | (drepl=>repl+ {frll = frll} ind lind)<br>removeCom {_} {_} {_} {_} {_} {frll} (_⊂_ {pll} {_} {_} {_} {ind} lf lf₁) (_←⊂ {_} {_} {_} {_} {_} {_} {_} {lind} ic) | .(replLL _ (ind +ᵢ lind) frll) | refl = ?<br>```<br><br></div><div>instead of :<br><br></div><div>```<br>removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) 
(_←⊂ {lind = lind} ic) with (replLL ll ind (replLL pll lind frll)) | 
(drepl=>repl+ {frll = frll} ind lind)<br>removeCom {frll = frll} (_⊂_ {pll = pll} {ll = ll} {ind = ind} lf lf₁) (_←⊂ {lind = lind} ic) | .(replLL _ (ind +ᵢ lind) frll) | refl = ?<br>```<br><br></div><div>I wonder if the behavior can be changed.<br></div></div></div>