(*** sle_isid_sn *)
corec lemma pr_sle_isi_sn:
- â\88\80f1. ð\9d\90\88â\9dªf1â\9d« → ∀f2. f1 ⊆ f2.
+ â\88\80f1. ð\9d\90\88â\9d¨f1â\9d© → ∀f2. f1 ⊆ f2.
#f1 * -f1
#f1 #g1 #Hf1 #H1 #f2 cases (pr_map_split_tl f2) *
/3 width=5 by pr_sle_weak, pr_sle_push/
(*** sle_inv_isid_dx *)
corec lemma pr_sle_inv_isi_dx:
- â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 ð\9d\90\88â\9dªf2â\9d« â\86\92 ð\9d\90\88â\9dªf1â\9d«.
+ â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 ð\9d\90\88â\9d¨f1â\9d©.
#f1 #f2 * -f1 -f2
#f1 #f2 #g1 #g2 #Hf * * #H
[2,3: elim (pr_isi_inv_next … H) // ]