proposition: Lemma setX1_canon_axiom x a: lf_axiom (fun i => cst_graph (singleton a) i) x (product1 x a).
proof: Proof. move=> y yx; apply /setX1_P;split; aww; rewrite LgV;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)