proposition: Lemma species_of_structure_typification n A S R x s : species_of_structure n A S R -> (Typification n A S x s <-> (slistpl x n /\ inc s (echelon_of_base S (slist_append x A)))).
proof: Proof. move => [h1 h2 h3 h4]; split. by move => [u1 u2]; rewrite/Typ_scheme; Ytac0. by move => [qa qb]; rewrite/Typification /Typ_scheme; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)