fact: Fixpoint iter_respectful {S T} (A : relation S) (Z : relation T) (n : nat) : relation (iter_arrow_type n S T) := if n is n'.+1 then respectful A (@iter_respectful _ _ A Z n') else Z.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)