simpAll
We need another `update stage0` to remove workaround at `AC.lean`
mkImpDepCongrCtx
mkImpCongrCtx
rfl
simp
trace[Meta.debug]