pub fn dcs_ext_decidable_eq_basic( add: &mut impl FnMut(&str, Expr) -> Result<(), String>, ) -> Result<(), String>