-ntheorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
-#A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
-##[ @; ##| nassumption; ##]
-nqed.
+theorem sym_eq: ∀A:Type[2].∀x,y:A. x = y → y = x.
+#A; #x; #y; #Heq; apply (rewrite_l A x (λz.z=x));
+[ @ | assumption ]
+qed.