proposition: Lemma Eq_squareE x : (coarse x) \Eq (functions C2 x).
proof: Proof. apply:EqS. exists (Lf (fun z => (J (Vf z C0) (Vf z C1))) (functions C2 x) (coarse x)). move:(set2_1 C0 C1)(set2_2 C0 C1); rewrite -/C2 => i1 i2. saw; apply: lf_bijective. + move => f/functionsP[ff sf tf]; apply:setXp_i; Wtac. + move => f g/functionsP[ff sf tf] /functionsP[fg sg tg]. move /pr12_def =>[va vb]; apply: function_exten => //; try ue. by rewrite sf => y /set2_P; case => ->. + move => y /setX_P[py y1 y2]. have ax: lf_axiom (variant C0 (P y) (Q y)) C2 x. by move => t xtp; try_lvariant xtp. exists (Lf (variant C0 (P y) (Q y)) C2 x). by apply /functionsP; saw; apply: lf_function. by rewrite ! LfV//; aw; rewrite py. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)