/2 width=1 by pr_pat_eq, pr_eq_refl/ qed.
(* Inversions with pr_id ****************************************************)
(*** id_inv_at *)
lemma pr_pat_inv_id (f):
/2 width=1 by pr_pat_eq, pr_eq_refl/ qed.
(* Inversions with pr_id ****************************************************)
(*** id_inv_at *)
lemma pr_pat_inv_id (f):