/3 width=3 by pr_isi_inv_eq_id, pr_pat_id, pr_pat_eq_repl_back/
qed-.
(* Destructions with pr_pat *************************************************)
(*** isid_inv_at_mono *)
/3 width=3 by pr_isi_inv_eq_id, pr_pat_id, pr_pat_eq_repl_back/
qed-.
(* Destructions with pr_pat *************************************************)
(*** isid_inv_at_mono *)