proposition: Lemma freeg_rect_dom0 D: P D.
proof: Proof. apply: (@freeg_rect_dom _ _ xpred0) => [{}D|k x {}D]. move=> domD; congr P: H0; apply/esym/eqP; rewrite -dom_eq0. by case: (dom D) domD => [//|p ps] /(_ p); rewrite !inE eqxx. by move=> ? ? _; apply: HS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)