Yes, that's pretty much it. Doing this systematically for all types including dependent types that quantify over Bool, as well as for user defined higher inductive types is another matter.