proposition: Lemma ser_R3 : forall w, exists v, R3 w v.
proof: Proof. case => [[|[|[|n]]]] // i; by [exists ord0| exists (Ordinal (erefl (2 < 3)))]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)