How to prove a certain property of two sequences with equal length

[FliegendeWurst]

I would like to prove the below taclet in KeY.
The taclet assumes there are two sequences s1 and s2 such that:

• they have the same length
• every element of s1 is contained in s2
• s1 has no duplicate elements

It follows that:

• every element of s2 is contained in s1

    \lemma
    seqPerm_existsLemma {
        \schemaVar \term Seq s1, s2;
        \schemaVar \variables int i, j, k;
        \varcond( \notFreeIn (i,s1),\notFreeIn (i,s2),\notFreeIn (j,s1),\notFreeIn (j,s2),\notFreeIn (k,s1),\notFreeIn (k,s2)  )
        \add(
            ((s1.length = s2.length)
            & (\forall i; (0 <= i & i < s1.length -> (\exists k; (0 <= k & k < s2.length & s1[i] = s2[k]))))
            & (\forall i; (0 <= i & i < s1.length -> (\forall j; (0 <= j & j < s1.length -> (i = j | s1[i] != s1[j]))))))
            -> (\forall k; (0 <= k & k < s2.length -> (\exists i; (0 <= i & i < s1.length & s1[i] = s2[k]))))
            ==>
        )
    };

For s1.length <= 1, I can prove it in KeY. For larger values (tested up to s1.length = 5) I need Z3. I don't know how I could go about solving the general case.

[wadoon]

First of all, your Taclet is rather written as an axiom. The Taclet does not assume anything or find anything. It just brings a formula to the sequent. So you want to prove that this formula always holds.

To prove this axiom, I guess the way is by using induction over the length of s1 and s2. But the induction step is not trivial, and I do not see the re-use of the induction step directly. Seems to be an HOL/rocq/... problem.

[WolframPfeifer]

In a recent meeting, it was indeed possible to prove this via induction (although quite tricky) directly in KeY. Thanks, @wadoon, for the hint!