proposition: Lemma set1_order_is x y: (singleton (J x x)) \Is (singleton (J y y)).
proof: Proof. have [[o1 _] s1] := (set1_wor x). have [[o2 _] s2] := (set1_wor y). have ta: lf_axiom (fun _ => y) (singleton x) (singleton y) by move=> t;fprops. exists (Lf (fun _ => y) (singleton x) (singleton y)). split => //. rewrite s1 s2; split; aw => //. apply lf_bijective => //. by move=> u v /set1_P -> /set1_P ->. move=> t /set1_P ->; exists x;fprops. hnf; rewrite lf_source => a b pa pb; rewrite !LfV // (set1_eq pa) (set1_eq pb). by split; move => _; apply:set1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)