(*** coafter_fwd_isid2_O_aux *)
corec fact pr_coafter_des_ist_sn_isi_unit_aux:
- ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
+ ∀f1. @⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
#f1 #H1f1 #f2 #f #H #H2f1 #Hf
cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
(*** coafter_fwd_isid2_aux *)
fact pr_coafter_des_ist_sn_isi_aux:
- (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
- ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
+ (∀f1. @⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
+ ∀i2,f1. @⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
#i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1