(*** H_coafter_isfin2_fwd *)
definition H_pr_coafter_des_ist_isf: predicate pr_map ≝
- λf1. â\88\80f2. ð\9d\90\85â\9dªf2â\9d« â\86\92 ð\9d\90\93â\9dªf1â\9d« â\86\92 â\88\80f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+ λf1. â\88\80f2. ð\9d\90\85â\9d¨f2â\9d© â\86\92 ð\9d\90\93â\9d¨f1â\9d© â\86\92 â\88\80f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
(* Destructions with pr_ist and pr_isf **************************************)
(*** coafter_isfin2_fwd_O_aux *)
fact pr_coafter_des_ist_isf_unit_aux:
- â\88\80f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
+ â\88\80f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
#f1 #Hf1 #f2 #H
generalize in match Hf1; generalize in match f1; -f1
@(pr_isf_ind … H) -f2
(*** coafter_isfin2_fwd_aux *)
fact pr_coafter_des_ist_isf_aux:
- (â\88\80f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
- â\88\80i2,f1. @â\9dªð\9d\9f\8f, f1â\9d« ≘ i2 → H_pr_coafter_des_ist_isf f1.
+ (â\88\80f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
+ â\88\80i2,f1. @â\9d¨ð\9d\9f\8f, f1â\9d© ≘ i2 → H_pr_coafter_des_ist_isf f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #f2 #Hf2 #H2f1 #f #Hf
elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1