(*** H_after_inj *)
definition H_pr_after_inj: predicate pr_map ≝
- λf1. ð\9d\90\93â\9dªf1â\9d« →
- â\88\80f,f21,f22. f1 â\8a\9a f21 â\89\98 f â\86\92 f1 â\8a\9a f22 â\89\98 f â\86\92 f21 â\89¡ f22.
+ λf1. ð\9d\90\93â\9d¨f1â\9d© →
+ â\88\80f,f21,f22. f1 â\8a\9a f21 â\89\98 f â\86\92 f1 â\8a\9a f22 â\89\98 f â\86\92 f21 â\89\90 f22.
(* Main destructions with pr_ist ********************************************)
(*** after_inj_O_aux *)
corec fact pr_after_inj_unit_aux:
- ∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_pr_after_inj f1.
+ ∀f1. @⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1.
#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [|*: // ] #g1 #H1
lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
(*** after_inj_aux *)
fact pr_after_inj_aux:
- (∀f1. @❪𝟏, f1❫ ≘ 𝟏 → H_pr_after_inj f1) →
- ∀i2,f1. @❪𝟏, f1❫ ≘ i2 → H_pr_after_inj f1.
+ (∀f1. @⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1) →
+ ∀i2,f1. @⧣❨𝟏, f1❩ ≘ i2 → H_pr_after_inj f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [|*: // ] #g1 #H1g1 #H1