proposition: Lemma Exercise1_5d r: order r -> order_morphism (Lf singleton (substrate r) (free_subsets r)) r (free_subset_order r).
proof: Proof. move=> or. have tf: (lf_axiom singleton (substrate r) (free_subsets r)). by move=> x xsr; apply: Exercise1_5b. have [pa pb] :=(fs_order_osr or). split => //; first by split;aw => //; apply: lf_function. hnf; aw;move=> x y xsr ysr; rewrite !LfV//;apply: (Exercise1_5cP or xsr ysr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)