proposition: Lemma R1 (s : sform) : R [fset s] = if s is fAX u^+ then [fset u^+] else fset0.
proof: Proof. case: s => [[|p|s t|s|s] [|]]; by rewrite /R sep1 /= ?fimset1 ?fimset0. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)