-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e)" with precedence 19 for @{ 'Or_elim $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
-interpretation "Or_elim" 'Or_elim ab ac bc c = (cast c (Or_elim _ _ _ ab ac bc)).
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
+interpretation "Or_elim" 'Or_elim ab \eta.ac \eta.bc c = (cast c (Or_elim _ _ _ ab ac bc)).