proposition: Lemma sub_free_subsets r X Y: inc X (free_subsets r) -> sub Y X -> inc Y (free_subsets r).
proof: Proof. move => /free_subsetsP[Xs Fr] YX. apply/free_subsetsP; split; first by apply: (sub_trans YX Xs). by move => x y /YX xX /YX yX le; apply: Fr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)