(* Constructions with pr_id *************************************************)
(*** id_at *)
-lemma pr_pat_id (i): @❪i,𝐢❫ ≘ i.
+lemma pr_pat_id (i): @⧣❨i,𝐢❩ ≘ i.
/2 width=1 by pr_pat_eq, pr_eq_refl/ qed.
(* Inversions with pr_id ****************************************************)
(*** id_inv_at *)
lemma pr_pat_inv_id (f):
- (∀i. @❪i,f❫ ≘ i) → 𝐢 ≡ f.
+ (∀i. @⧣❨i,f❩ ≘ i) → 𝐢 ≐ f.
/3 width=1 by pr_pat_inv_eq, pr_id_eq/
qed-.