proposition: Lemma tc_cond x y : tc x y -> (x \in h) = (y \in h).
proof: Proof. by case/tc_closed/andP=>->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq choice fintype path fingraph) pcm(options axioms pred prelude finmap seqext)