proposition: Lemma well_founded_iterated_prod_relationA_of B (sz : B -> nat) (f : forall b, iterated_prod (sz b)) : well_founded (@iterated_prod_relationA_of B sz f).
proof: Proof. intro b. pose proof (@well_founded_RA_of_opt (iterated_prod (sz b)) iterated_prod_relationA B) as wf. specialize (wf (fun b' => match nat_eq_transfer _ (sz b') (sz b) (f b') with | inl v => Some v | inr _ => None end)). specialize (wf well_founded_iterated_prod_relationA). eapply Acc_subrelation; [ eapply wf | clear wf ]. intros x y H. apply RT_closure_same_size in H. unfold iterated_prod_relationA_of. generalize dependent (f b). generalize dependent (f x). generalize dependent (f y). generalize dependent (sz y). intros ??; subst. clear y. generalize dependent (sz b). generalize dependent (sz x). clear. handle_nat_eq_transfer. rewrite !nat_eq_transfer_refl in *. assumption. Defined.
imports: Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf Coq.Lists.SetoidList Coq.Arith.PeanoNat Fiat.Common.Coq__8_4__8_5__Compat