(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ ~ ⬊ * break [ term 46 o , break term 46 h , break term 46 f ] 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 $o $f $G $L }.