#A #x #P #Hx #y #Heq (cases Heq); //; qed.
theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
#A #x #P #Hx #y #Heq (cases Heq); //; qed.
theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.