proposition: Lemma Eq_set1 x : singleton x \Eq C1.
proof: Proof. exists (Lf (fun _ => C0) (singleton x) C1); saw. apply:lf_bijective. - move => t _; apply:set1_1. - by move => u v /set1_P -> /set1_P -> _. - move => y /set1_P ->; exists x => //; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)