proposition: Lemma Exercise1_15a17: lf_axiom lobs (substrate r) (substrate (completion_order r)).
proof: Proof. move=> t tsr; rewrite /completion_order (proj2(sub_osr _)). by apply: Exercise1_15a8; apply: set1_sub. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)