(*** at_id_fwd *)
lemma pr_pat_id_des (i1) (i2):
- @â\9dªi1,ð\9d\90¢â\9d« ≘ i2 → i1 = i2.
+ @â\9d¨i1,ð\9d\90¢â\9d© ≘ i2 → i1 = i2.
/2 width=4 by pr_pat_mono/ qed-.
(* Main constructions with pr_id ********************************************)
(*** at_div_id_dx *)
theorem pr_pat_div_id_dx (f):
- H_pr_pat_div f 𝐢 𝐢 f.
+ H_pr_pat_div f (𝐢 ) (𝐢) f.
#f #jf #j0 #j #Hf #H0
lapply (pr_pat_id_des … H0) -H0 #H destruct
/2 width=3 by ex2_intro/
(*** at_div_id_sn *)
theorem pr_pat_div_id_sn (f):
- H_pr_pat_div 𝐢 f f 𝐢.
+ H_pr_pat_div (𝐢) f f (𝐢).
/3 width=6 by pr_pat_div_id_dx, pr_pat_div_comm/ qed-.