fact: Definition pi3 (n : nat) : 'I_3 := match n with | 0 => ord0 | n.+1 => if [exists m : 'I_n, f m] then Ordinal (erefl (2 < 3)) else if f n then Ordinal (erefl (1 < 3)) else ord0 end.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)