proposition: Lemma Exercise4_8l: inc E48z (substrate E48AJIo).
proof: Proof. move: Exercise4_8k => [[_ p1] _ ]; rewrite p1. have s1: sub (irreds r) (substrate r) by apply: Zo_S. have ta: lf_axiom (fun _ : Set => \0c) (irreds r) E48I. rewrite /E48I;move=> t _; fprops. apply /(Exercise4_8iP s1); rewrite /E48z; saw. by apply: lf_function. move => i j ii ji; rewrite !LfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)