[WP] adds one more test

src/plugins/wp/tests/wp_plugin/nth.i

@@ -57,7 +57,8 @@
                                    <==> (A ^ B ^ C ^ S ^ S) == S ;
 
 
-
+  check lemma subsequence1: ko: ( A ^ (S *^ N) ^ B ^ S ^ C ) == ( (S *^ N) ^ S )
+                           <==> ( A ^ B ^ C ^ C ) == C ;
 
   }
 */

src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle

@@ -51,6 +51,11 @@ Prove: let a_0 = (concat L_B L_A L_S) in
 Lemma right_unfold_repeat2:
 Prove: true
 
+------------------------------------------------------------
+
+Lemma subsequence1:
+Prove: true
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Axiomatic 'MkRepeat'