(* elim H. BUG DI UNSHARING *)
(*apply (ledx_ind (\lambda x.\lambda y. n=x \to O=y \to x=y) ? ? ? ? H).*)
simplify. intros. reflexivity.
(* elim H. BUG DI UNSHARING *)
(*apply (ledx_ind (\lambda x.\lambda y. n=x \to O=y \to x=y) ? ? ? ? H).*)
simplify. intros. reflexivity.