If we go for example to http://logipedia.inria.fr/sttfa_bool__cases_term_6.def.html then both "Body" and "Type_annotation" show: Missing open brace for subscript
If we go for example to
http://logipedia.inria.fr/sttfa_bool__cases_term_6.def.html
then both "Body" and "Type_annotation" show: