proposition: Lemma cst_graph_pr x y: cst_graph x y = x *s1 y.
proof: Proof. set_extens t. by move/funI_P => [z zx ->]; apply: indexed_pi. move /indexed_P => [pt Pt Qt];apply/funI_P; ex_tac; rewrite - Qt //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)