- | -HLK1 -HVT1 * #I2 #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded
- [ -Hd1 -Hde2
- lapply (transitive_le … Hded Hd2) -Hded -Hd2 #H
- lapply (lt_to_le_to_lt … Hde1 H) -Hde1 -H #H
- elim (lt_refl_false … H)
- | -Hd2 -Hde1
- lapply (transitive_le … Hded Hd1) -Hded -Hd1 #H
- lapply (lt_to_le_to_lt … Hde2 H) -Hde2 -H #H
- elim (lt_refl_false … H)
+ | -HLK1 -HVT1 * #I2 #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded [ -Hd1 -Hde2 | -Hd2 -Hde1 ]
+ [ elim (ylt_yle_false … Hde1) -Hde1 /2 width=3 by yle_trans/
+ | elim (ylt_yle_false … Hde2) -Hde2 /2 width=3 by yle_trans/