proposition: Lemma ssub'_refl s b : (s,b) \in ssub' b s.
proof: Proof. case: s => [|x|s t|s|s t|s t] /=; by rewrite !inE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)