@@ -106,7 +106,6 @@ sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
106106 -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
107107 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
108108 -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
109− f Z acc y pf = absurd pf
110109 f (S n) (Access acc) y (LTESucc yLEx)
111110 = Access (\z, zLTy =>
112111 f n (acc n $ LTESucc lteRefl) z (lteTransitive zLTy yLEx)
@@ -117,7 +116,6 @@ sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
117116 ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
118117 where
119118 ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
120− ltAccessible' Z x = absurd x
121119 ltAccessible' (S k) (LTESucc x)
122120 = Access (\val, p => ltAccessible' k (lteTransitive p x))
123121