axiom a: A.
axiom b: B.
+include "logic/connectives.ma".
notation "#" non associative with precedence 90 for @{ 'sharp }.
interpretation "a" 'sharp = a.
interpretation "b" 'sharp = b.
-ntheorem prova : ((A â\86\92 A → B) → (A → B) → C) → C.
+ntheorem prova : ((A â\88§ A → B) → (A → B) → C) → C.
# H;
-napply (H ? ?) [#L | #K1; #K2]
+napply (H ? ?) [#L | *w; #K1; #K2]
napply #.
nqed.
\ No newline at end of file