proposition: Lemma identity_prop0 E f: function_prop f E E -> (forall x, inc x E -> (Vf f x) = x) -> f = identity E.
proof: Proof. move: (identity_prop E) => [fa sa ta] [fb sb tb] fv. apply:function_exten => //; try ue. by rewrite sb => x xE; bw =>//; apply: fv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)