proposition: Lemma GE_prop6 E s z z': inc z E -> unit E s z -> inc z' E -> unit E s z' -> z = z'.
proof: Proof. by move => sa sb sc sd; rewrite - (proj1 (sb _ sc)) (proj2 (sd _ sa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)