proposition: Lemma setC1_proper A x : inc x A -> ssub (A -s1 x) A.
proof: Proof. move => xa; split; first by apply: sub_setC. move => eq1; move: xa; rewrite -eq1; exact: setC1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)