(* 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-.