(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( â¦\83 term 46 G1, break term 46 L1, break term 46 T1 â¦\84 â\89\9b â¦\83 break term 46 G2, break term 46 L2, break term 46 T2 â¦\84 )"
+notation "hvbox( â\9dª term 46 G1, break term 46 L1, break term 46 T1 â\9d« â\89\9b â\9dª break term 46 G2, break term 46 L2, break term 46 T2 â\9d« )"
non associative with precedence 45
for @{ 'StarEqSn $G1 $L1 $T1 $G2 $L2 $T2 }.