<div dir="ltr">Hey all,<div><br></div><div>i've a small development (a baby system f), </div><div>and I find myself with a case that looks like the following (full file attached, key bit inline here)</div><div><br></div><div><br></div><div><div>τSubstFancy : ∀  { tfv } -> (barrier : Nat) -> TypeF (1  + barrier  + tfv ) -> TypeF ( barrier + tfv) -> TypeF (barrier + tfv )</div><div>τSubstFancy bar (vτ x) t  with compare bar (finToNat x)</div><div>τSubstFancy zero (vτ zero) t | less lt = {!!} -- this is the case i'm stumped by</div></div><div><div>τSubstFancy zero (vτ (suc x)) t | less lt = {!!}</div><div>τSubstFancy (suc bar) (vτ x) t | less lt = {!!}</div><div>τSubstFancy bar (vτ x) t | equal eq = t</div><div>τSubstFancy bar (vτ x) t | greater gt = {!!}</div><div>τSubstFancy bar (∀τ tar) t = {!!}</div><div>τSubstFancy bar (tar →τ tar₁) t = {!!}</div></div><div><br></div>how do i deal with this  0 < 0 case?<div>it seems like it should be absurd, but the syntax doens't quite work, </div><div><br></div><div>also this is using ulf's agda prelude lib atm, but that shouldn't be relevant to this question.</div><div><br></div><div>Or is this a bug? :)</div><div><br></div><div>many thanks</div><div>-Carter</div><div><br></div><div><br></div></div>