-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.