fact: Parameter Fix : forall G A (B : A -> Type) (s : forall x : A, spec G (B x)), ((forall x : A, STspec G (s x)) -> forall x : A, STspec G (s x)) -> forall x : A, STspec G (s x).
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)