+notation "mstyle color #007f00 (hvbox(e ⊢ ♦))"
+ non associative with precedence 30 for @{ 'wfejudg $e }.
+interpretation "Fsub WF env judgement" 'wfejudg e = (WFEnv e).
+
+notation "mstyle color #007f00 (hvbox(e ⊢ break t))"
+ non associative with precedence 30 for @{ 'wftjudg $e $t }.
+interpretation "Fsub WF type judgement" 'wftjudg e t = (WFType e t).
+
+notation > "\Forall S.T"