(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ ~ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )"
+notation "hvbox( G ⊢ ~ ⬊ * [ break term 46 h , break term 46 o , break term 46 f ] break term 46 L )"
non associative with precedence 45
- for @{ 'CoSN $h $g $d $G $L }.
+ for @{ 'CoSN $h $o $f $G $L }.