proposition: Lemma RcE C a s : (s^+ \in Rc a C) = ([(pV a)^^]s^+ \in C).
proof: Proof. apply/fimsetP/idP => [ [t] | H]. - rewrite inE andbC. by case: (isCBoxP a t) => //= t' -> /= ? [->]. - exists ([(pV a)^^]s^+) => //. by rewrite inE H /=. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)