I'm struggling sooo much because accessibility predicates aren't definitionally equal and I can't FORCE them to be equal in Agda as;ldhskdajga

yeah, I can transport along propositional equalities. but then what? my proofs are littered with the corpses of abandonded congs

@ionchy embrace the REWRITE

@totbwf I can't rewrite by ∀ {k} {p q : Acc k} → p ≡ q 😩​

@ionchy 😔

@ionchy assuming that Prop is a no go?

@totbwf not for accessibility, it seems
I also do induction on Acc and putting it in Prop would prevent me from eliminating to anything useful