@⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
#L1 #L #des #H elim H -L1 -L -des
[ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/
@⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
#L1 #L #des #H elim H -L1 -L -des
[ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/