proposition: Lemma transportable_typificationg n A S: Typ_auxg n A S -> Transportableg n A S (Typificationg n A S).
proof: Proof. move => h x s y f H; move:(transportable_aux1 H) => h1. by split => //; case:H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)