I’ve thought about how to let folks prove to Fil-C that Fil-C’s checks are obviated by some higher level checks.

It’s a super hard problem! I don’t have a good answer, but I also can’t prove that it’s impossible