(* Inversions with pr_eq ****************************************************)
(* Note: this has the same proof of the previous *)
(* Inversions with pr_eq ****************************************************)
(* Note: this has the same proof of the previous *)