proposition: Lemma RE C s : (s^+ \in R C) = (fAX s^+ \in C).
proof: Proof. apply/fimsetP/idP => [ [t] | H]. - rewrite inE andbC. by case: (isBoxP t) => //= t' -> /= ? [->]. - exists (fAX s^+) => //. by rewrite inE H. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)