proposition: Lemma well_founded_iterated_prod_relationA_of_opt {B n f} : well_founded (@iterated_prod_relationA_of_opt B n f).
proof: Proof. unfold iterated_prod_relationA_of_opt. apply well_founded_RA_of_opt, well_founded_iterated_prod_relationA. 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