@@ -106,7 +106,6 @@ sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
106 -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
106 -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
107 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
107 f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
108 -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
108 -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
109− f Z acc y pf = absurd pf
110 f (S n) (Access acc) y (LTESucc yLEx)
109 f (S n) (Access acc) y (LTESucc yLEx)
111 = Access (\z, zLTy =>
110 = Access (\z, zLTy =>
112 f n (acc n $ LTESucc lteRefl) z (lteTransitive zLTy yLEx)
111 f n (acc n $ LTESucc lteRefl) z (lteTransitive zLTy yLEx)
@@ -117,7 +116,6 @@ sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
117 ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
116 ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
119 ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
118 ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
120− ltAccessible' Z x = absurd x
121 ltAccessible' (S k) (LTESucc x)
119 ltAccessible' (S k) (LTESucc x)
122 = Access (\val, p => ltAccessible' k (lteTransitive p x))
120 = Access (\val, p => ltAccessible' k (lteTransitive p x))