(*** at_id_fwd *)
lemma pr_pat_id_des (i1) (i2):
- @âªi1,ð¢â« â i2 â i1 = i2.
+ ïŒ â§£âši1,ð¢â© â 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-.