| #f1 #I1 #L1 #V1 #Hf1 #IH #I2 #L2 #V2 *
[ -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
#H destruct #g1 #Hgf1 >(injective_next … Hgf1) -g1
- /2 width=3 by sle_refl, ex2_intro/
+ /3 width=3 by sle_refl, ex2_intro/
| -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
#HL12 #g1 <tls_xn <tl_next_rew #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
/2 width=3 by ex2_intro/
elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
- /3 width=6 by sor_sle_sn, ex2_intro/
+ /3 width=6 by sor_inv_sle_sn_trans, ex2_intro/
| -IHV1 #_ >tls_xn #H2 elim (IHT1 … H2) -IHT1 -H2
- /3 width=6 by drops_drop, sor_sle_dx, ex2_intro/
+ /3 width=6 by drops_drop, sor_inv_sle_dx_trans, ex2_intro/
]
| #fV1 #fT1 #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHV1 #IHT1 #I2 #L2 #V2 #n #HL12 #g1 #Hgf1
lapply (sor_tls … Hf1 n) -Hf1 <Hgf1 -Hgf1 #Hf1
elim (sor_xxn_tl … Hf1) [1,2: * |*: // ] -Hf1
#gV1 #gT1 #Hg1
[ -IHT1 #H1 #_ elim (IHV1 … HL12 … H1) -IHV1 -HL12 -H1
- /3 width=6 by sor_sle_sn, ex2_intro/
+ /3 width=6 by sor_inv_sle_sn_trans, ex2_intro/
| -IHV1 #_ #H2 elim (IHT1 … HL12 … H2) -IHT1 -HL12 -H2
- /3 width=6 by sor_sle_dx, ex2_intro/
+ /3 width=6 by sor_inv_sle_dx_trans, ex2_intro/
]
]
qed-.