fact: Definition Typ_hypg n x A S s y f := [/\ Typificationg n A S x s, slistpl y n, slistpl f n & forall i, i <c n -> inc (Vg f i) (bijections (Vg x i) (Vg y i))].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)