Proving an iterative algorithm with recursive functions (Dafny)

I have this algorithm that computes the product of the unique numbers in a given integer array:

method UniqueProduct(a: array<int>) returns (product: int)
requires a.Length > 0
ensures product == ProductOfUniques(a[..])
{
var p := 1;
var seen: seq<int> := [];
for i := 0 to a.Length
invariant 0 <= i <= a.Length
invariant forall x :: x in seen ==> x in a[..i]
invariant forall k :: 0 <= k < i && a[k] !in seen ==> seen == a[..i]
invariant forall k :: 0 <= k < i && a[k] !in seen ==> p == ProductOfUniques(a[..i])
//        invariant p == ProductOfUniques(a[..i])
{
if !(a[i] in seen) {
seen := seen + [a[i]];
p := p * a[i];
}
assert a[..i+1][..i] == a[..i];
assert forall k :: 0 <= k < |seen| ==> seen[k] in a[..i+1];
assert a[i] !in seen ==> p == ProductOfUniques(a[..i+1]) == ProductOfUniques(a[..i]+[a[i]]);
assert a[i] in seen <== p == ProductOfUniques(a[..i]);
}
assert a[..a.Length] == a[..];
assert a[a.Length-1] !in seen ==> p == ProductOfUniques(a[..a.Length]) == ProductOfUniques(a[..a.Length-1]+[a[a.Length-1]]);
assert a[a.Length-1] in seen <== p == ProductOfUniques(a[..a.Length-1]+[a[a.Length-1]]);
//    assert p == ProductOfUniques(a[..]);
product := p;
}

And these functions:

ghost function ProductOfUniques(a: seq<int>) : int
{
if |a| == 0 then 1 
else Multiply(a, [])
}
ghost function Multiply(numbers: seq<int>, seen: seq<int>) : int
requires |numbers| > 0
{
var tail := numbers[|numbers|-1];
if |numbers| == 1 then 
if tail in seen then 1 else tail 
else 
Multiply(numbers[..|numbers|-1], seen + [tail]) * (if tail in seen then 1 else tail) 
}

All the individual assertions and invariants hold, but the method's postcondition does not verify. I can't, for the life of me, figure out how to convince Dafny to assert that this is true p == ProductOfUniques(a[..i]).

I tried writing a lemma that would assert

lemma X(a: seq<int>, i: int, n: int)
requires |a| > 0
requires 0 < i < |a|
ensures n in a[..i] ==> ProductOfUniques(a[..i]) == ProductOfUniques(a[..i] + [n])

But this also led me to a dead end.
Any help appreciated. Thanks.

Following two lemmas of for loop are valid by being vacuous.

invariant forall k :: 0 <= k < i && a[k] !in seen ==> seen == a[..i]
invariant forall k :: 0 <= k < i && a[k] !in seen ==> p == ProductOfUniques(a[..i])

If you replace conclusion with false it still goes through like shown below

invariant forall k :: 0 <= k < i && a[k] !in seen ==> false

This means these two invariants are not that useful.

There is data structure in dafny which holds unique element namely set. In solution below I will be using set instead of sequence.

With program below I am getting verification error that third invariant is not being maintained.

method UniqueProduct (arr: array<int>) returns (product: int)
ensures product == SetProduct((set i | 0 <= i < arr.Length :: arr[i]))
{
var p := 1;
var seen: set<int> := {};
for i := 0 to arr.Length
invariant 0 <= i <= arr.Length
invariant seen == (set k | 0 <= k < i :: arr[k])
invariant p == SetProduct((set k | 0 <= k < i :: arr[k]))
{
if ! (arr[i] in seen) {
seen := seen + { arr[i] };
p := p * arr[i];
}
}
product := p;
}
ghost function SetProduct(s : set<int>) : int
{
if s == {} then 1
else var x :| x in s; 
x * SetProduct(s - {x})
}

This means Dafny need some help to prove invariant being maintained. To assure myself that I am following right path I added below lemma without proof and invoke SetProductLemma(seen, arr[i]) as last statement inside if, it goes through.

lemma SetProductLemma(s: set <int>, x: int) 
requires x in s
ensures SetProduct(s - {x}) * x == SetProduct(s)

Now proving SetProductLemma is little tricky due to operator. I would point to read
https://leino.science/papers/krml274.html.

Full program is listed below

method UniqueProduct (arr: array<int>) returns (product: int)
ensures product == SetProduct((set i | 0 <= i < arr.Length :: arr[i]))
{
var p := 1;
var seen: set<int> := {};
for i := 0 to arr.Length
invariant 0 <= i <= arr.Length
invariant seen == (set k | 0 <= k < i :: arr[k])
invariant p == SetProduct((set k | 0 <= k < i :: arr[k]))
{
if ! (arr[i] in seen) {
seen := seen + { arr[i] };
p := p * arr[i];
SetProductLemma(seen, arr[i]);
}
}
product := p;
}
ghost function SetProduct(s : set<int>) : int
{
if s == {} then 1
else var x :| x in s; 
x * SetProduct(s - {x})
}
lemma SetProductLemma(s: set <int>, x: int) 
requires x in s
ensures SetProduct(s - {x}) * x == SetProduct(s)
{
if s != {}
{
var y :| y in s && y * SetProduct(s - {y}) == SetProduct(s);
if y == x {}
else {
calc {
SetProduct(s);
y * SetProduct(s - {y});
{ SetProductLemma(s - {y}, x); }
y * x * SetProduct(s - {y} - {x});
{ assert s - {x} - {y} == s - {y} - {x};}
y * x * SetProduct(s - {x} - {y});
x * y * SetProduct(s - {x} - {y});
{ SetProductLemma(s - {x}, y); }
x * SetProduct(s - {x});
}
}
}
}