+
+notation > "[H]" with precedence 90
+for @{ assumpt ? (cast ? ? $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 $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 (? ∧ False) $ab ?) }.
+notation > "∧\sub\e\sup\l term 90 a ∧ term 90 b" with precedence 19
+for @{ And_elim_l ?? (cast (? ∧ $b) ($a ∧ $b) ?) }. *)
+notation > "∧\sub\e\sup\l term 90 ab" with precedence 19
+for @{ And_elim_l ?? (cast $ab $ab ?) }. (* CSC: WRONG *)
+notation > "∧\sub\e\sup\r term 90 ab" with precedence 19
+for @{ And_elim_r ?? (cast $ab $ab ?) }. (* CSC: WRONG *)
+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 $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 $ab ?) }. (* CSC: WRONG *)
+notation > "∃\sub\e term 90 enpn [ident z] [ident pz] term 90 c" with precedence 19
+for @{ Exists_elim ??? (cast $enpn $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 ?) }.
+