proposition: Lemma transportable_spec1 n A S R: n = \0c -> Typ_auxg n A S -> Transportableg n A S R.
proof: Proof. move => nz [ha hb hc hd] x s y f [[pa pb pc pd] hf hg _]. rewrite nz in hf pb. rewrite (slist_emptyp (proj1 pb) (proj2 pb)). rewrite (slist_emptyp (proj1 hf) (proj2 hf)). rewrite /Typ_concg; set s' := Lg _ _. move: pc => [pc1 pc2]. have dd1: domain s = domain S. by rewrite (slist_domain pc1) pc2 (slist_domain hc). have dd: domain s = domain s' by rewrite /s' Lgd. suff: s = s' by move => ->; split. apply: fgraph_exten; [ exact (proj1 pc1) | rewrite /s'; fprops | done | ]. rewrite dd1; move => i ids /=; rewrite /s' LgV//. have lis: i <c slength s. apply /(NintP (slength_nat pc1)). by rewrite - (slist_domain pc1) dd1. move: (pd _ lis); rewrite /Typ_schemeg; Ytac sz; first by move/in_set0. rewrite nz in hg. move: (hd _ ids) => [ua]; rewrite nz => eq1 ww. by rewrite(Typ_with_id_prop2 pb hg hb ua sz eq1 (erefl \0c)) idV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)