(*** after_fwd_isid_sn *)
lemma pr_after_des_ist_eq_sn:
- â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f1 â\89¡ f → 𝐈❨f2❩.
+ â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f1 â\89\90 f → 𝐈❨f2❩.
#f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
#Hf2 #Hf1 #H @pr_isi_pat_total // -Hf2
#i2 #i #Hf2 elim (Hf1 i2) -Hf1
(*** after_fwd_isid_dx *)
lemma pr_after_des_ist_eq_dx:
- â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\89¡ f → 𝐈❨f1❩.
+ â\88\80f2,f1,f. ð\9d\90\93â\9d¨fâ\9d© â\86\92 f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\89\90 f → 𝐈❨f1❩.
#f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
#Hf2 #Hf1 #H2 @pr_isi_pat_total // -Hf1
#i1 #i2 #Hi12 elim (pr_after_des_ist_pat … Hi12 … Hf) -f1