proposition: Lemma mem_can_to x a l : x \in l -> C[x]_(a, l) \in l.
proof: Proof. move=> xIp1; rewrite /can_to. by case: (leqP (size l) (find (symconnect (relto a r) x) l)) => H1; [rewrite nth_default | rewrite mem_nth]. Qed.
imports: mathcomp(all_ssreflect) extra