I am (still) struggling with a recursive function on finite sets. I would like to define a special Cartesian product on a finite set of (finite) sets. A simplified example of what I am trying to achieve is the pcart function below:

theory Simplified
  imports Main "HOL-Library.FSet"
begin

inductive_set Fin where
  emptyI: "{} ∈ Fin" | 
  insertI: "A ∈ Fin ⟹ insert a A ∈ Fin"

lemma Fin_is_finite: "x ∈ Fin ⟹ finite x"
  using Fin.inducts by auto

lemma finite_is_Fin: "finite x ⟹ x ∈ Fin"
  by (metis Fin.simps Finp_Fin_eq finite_ne_induct)

definition ext :: "nat set ⇒ nat set set" where 
  "ext X = {{x}| x. x ∈ X}"

function pcart :: "nat set fset ⇒ nat set set" where 
  "pcart {||} = {}" | 
  "pcart (finsert a A) = ext a ∪ pcart A ∪ {{x}∪y| x y. x ∈ a ∧ y ∈ pcart A}"
  apply blast
  apply blast
  apply blast

The problem is the very last subgoal of the proof, which I have no clue how to deal with:

 ⋀a A aa Aa.
       finsert a A = finsert aa Aa ⟹
       ext a ∪ pcart_sumC A ∪ {{x} ∪ y |x y. x ∈ a ∧ y ∈ pcart_sumC A} =
       ext aa ∪ pcart_sumC Aa ∪ {{x} ∪ y |x y. x ∈ aa ∧ y ∈ pcart_sumC Aa}

My question is three folded:

1. Is there an easier way to define my recursive function so that I can show it terminates?
2. If not, is there a way to prove that my version terminates? What am I missing?
3. If 1 or 2 are possible, and I obtain a recursive terminating function pcart – how can I go about showing that pcart {||} = {}? I fake-terminated my current version with a sorry, then tried to use it in the simplest lemma I could think of: lemma "pcart {||} = {}". To which I get no proof. At this point, I am unsure if it’s because pcart definition is flawed (I hope that’s the case) or because some other issues I am unaware of.

Any suggestions will be both much appreciated and welcome.
Thank you