fact: Definition iterated_prod_relationA_of B (sz : B -> nat) (f : forall b, iterated_prod (sz b)) : relation B := fun x y => match nat_eq_transfer _ (sz x) (sz y) (f x) with | inl fx => iterated_prod_relationA fx (f y) | inr _ => False end.
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