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