lemma sex_co_isid (RN1) (RP1) (RN2) (RP2):
RP1 ⊆ RP2 →
- â\88\80f,L1,L2. L1 ⪤[RN1,RP1,f] L2 â\86\92 ð\9d\90\88â\9dªfâ\9d« →
+ â\88\80f,L1,L2. L1 ⪤[RN1,RP1,f] L2 â\86\92 ð\9d\90\88â\9d¨fâ\9d© →
L1 ⪤[RN2,RP2,f] L2.
#RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 //
#f #I1 #I2 #K1 #K2 #_ #HI12 #IH #H