If you have an instance of this lemma in the context of a larger proof where the prover was unable to prove such a step, I'd be interested in hearing about it.
<4>1. J \in Nat
<4>2. seq \in [ 1 .. J -> ( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) ) ]
<4>3. seq \in Seq(( 0 .. 9 ) \X ( 0 .. 9 ) \X ( ( 0 .. 9 ) \X ( 0 .. 9 ) )) BY <4>1, <4>2