proposition: Lemma RT_closure_same_size B (sz : B -> nat) (f : forall b, iterated_prod (sz b)) a b (H : RT_closure (iterated_prod_relationA_of sz f) a b) : sz a = sz b.
proof: Proof. induction H as [x y H | | ]. { unfold iterated_prod_relationA_of in *. generalize dependent (f x). generalize dependent (f y). generalize dependent (sz x). generalize dependent (sz y). handle_nat_eq_transfer. } { reflexivity. } { etransitivity; eassumption. } 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