proposition: Lemma R1 a (s : sform) : R a [fset s] = if s is [pV b]u^+ then if (a == b) then [fset u^+] else fset0 else fset0.
proof: Proof. case: s => [[|x|s t|[b|p0 p1|p0 p1|p|t] s] [|]]; rewrite /R sep1 /= ?fimset1 ?fimset0 //. case: (a == b); by rewrite ?fimset1 ?fimset0. Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)