proposition: Lemma Typ_with_id_empty x: slistp x -> Typ_with_id x emptyset = x.
proof: Proof. rewrite /Typ_with_id domain_set0 /Lg funI_set0;apply:slist_append_empty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq)