proposition: Lemma free_subsetsP r x: inc x (free_subsets r) <-> (sub x (substrate r) /\ free_subset r x).
proof: Proof. split; first by move=> /Zo_P[/setP_P ha hb]. by move => [ha hb]; apply/Zo_P; split => //; apply /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)