proposition: Lemma pure_properties_res3: exists A S, [/\ pure_prop1 A S, pure_prop2 S, pure_prop3 A S, pure_prop5 A S & ~ (pure_prop4 S)].
proof: Proof. have xx: (substrate (sub_order (singleton C2))) = (singleton C2). by rewrite (proj2 (sub_osr _)). exists C2; exists (singleton C2); split => //. by split; fprops; move => x /set1_P ->; fprops. move => h ha _; exists C2; hnf; rewrite xx;split;fprops. move => y yh; move: (ha _ yh); rewrite xx;aw; move /set1_P=> ->. by apply /sub_gleP;split;fprops. move => m n ma mn /set1_P ta /set1_P tb /set1_P tc. case: ta; apply: extensionality => //; rewrite -tc. by apply: subsetI2l. move => x xtp /set1_P xntp; exists emptyset; aw; split;fprops. apply: emptyset_finite. by move /set1_P => tpe; symmetry in tpe; empty_tac1 C0. move => h; move: (set1_1 C2) => ta. have tb: sub (singleton C0) C2 by move => t /set1_P ->; fprops. by move: inc_C1_C2; move: (h _ _ ta tb) => /set1_P <- /set1_P; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)