+
+notation > "[H]" with precedence 90
+for @{ assumpt ? $H}.
+notation > "⇒\sub\i [ident H] term 90 b" with precedence 19
+for @{ Imply_intro ?? (λ${ident H}.cast $b ?) }.
+notation > "⇒\sub\e term 90 ab term 90 a" with precedence 19
+for @{ Imply_elim ?? (cast $ab ?) (cast $a ?) }.
+notation > "∧\sub\i term 90 a term 90 b" with precedence 19
+for @{ And_intro ?? (cast $a ?) (cast $b ?) }.
+notation > "∧\sub\e\sup\l term 90 ab" with precedence 19
+for @{ And_elim_l ?? (cast $ab ?) }.
+notation > "∧\sub\e\sup\r term 90 ab" with precedence 19
+for @{ And_elim_r ?? (cast $ab ?) }.
+notation > "∨\sub\i\sup\l term 90 a" with precedence 19
+for @{ Or_intro_l ?? (cast $a ?) }.
+notation > "∨\sub\i\sup\r term 90 a" with precedence 19
+for @{ Or_intro_r ?? (cast $a ?) }.
+notation > "∨\sub\e term 90 ab [ident Ha] term 90 c1 [ident Hb] term 90 c2" with precedence 19
+for @{ Or_elim ??? (cast $ab ?) (λ${ident Ha}.cast $c1 ?) (λ${ident Hb}.cast $c2 ?) }.
+notation > "∀\sub\i [ident z] term 90 a" with precedence 19
+for @{ Forall_intro ?? (λ${ident z}.cast $a ?) }.
+notation > "∀\sub\e term 90 ab" with precedence 19
+for @{ Forall_elim ?? ? (cast $ab ?) }.
+notation > "∃\sub\e term 90 enpn [ident z] [ident pz] term 90 c" with precedence 19
+for @{ Exists_elim ??? (cast $enpn ?) (λ${ident z}.λ${ident pz}.cast $c ?) }.
+notation > "∃\sub\i term 90 n term 90 pn" with precedence 19
+for @{ Exists_intro ? (λ_.?) $n (cast $pn ?) }.
+