agda中的重写和等式推理

Question

通过重写,我有一个简洁的语法(例如,没有调用同余属性),我可以证明:

-- * is associative
*-assoc : ? a b c ? (a * b) * c ? a * (b * c)
*-assoc zero b c = refl
*-assoc (succ a) b c rewrite *+-dist b (a * b) c | *-assoc a b c = refl

但是,我的小脑子可以更好地解析这个证明

--written in equational style
*-assoc' : ? a b c ? (a * b) * c ? a * (b * c)
*-assoc' zero b c = refl
*-assoc' (succ a) b c = (succ a * b) * c  ?? refl ?
                        (b + a * b) * c ?? *+-dist b (a * b) c ?
                        b * c + (a * b) * c ?? cong (? x -> b * c + x) (*-assoc a b c)  ?
                        b * c + a * (b * c)  ?? refl ?
                        (succ a) * (b * c) ? 

但是我必须通过调用同余来指定"转换"哪个子项.

有没有办法结合重写和等式写作来摆脱一致性提及？

提前致谢