remove a believe_me

This commit is contained in:
rhiannon morris 2022-11-01 21:05:04 +01:00
parent e1a9d99514
commit e7272333cb

View file

@ -110,7 +110,14 @@ export
ssDownEqv SZ = EqSS EqSZ
ssDownEqv (SS by) = EqSS $ ssDownEqv by
%transform "Shift.ssDown" ssDown by = believe_me (SS by)
private
ssDownViaNat : Shift (S from) to -> Shift from to
ssDownViaNat by =
rewrite shiftDiff by in
rewrite sym $ plusSuccRightSucc by.nat from in
fromNat $ S by.nat
%transform "Shift.ssDown" ssDown = ssDownViaNat
public export