proposition: Lemma AR3_0 : cAR (@trans M3) (eval (fV 0)) (eval (fV 1)) ord0.
proof: Proof. cofix AR3_0. apply: ARs; first done. case. case => [|[|n]] i. - suff ->: Ordinal i = ord0. move => _. exact: AR3_0. congr Ordinal. exact: eq_irrelevance. - move => _. apply: AR0 => //. - move => H. case: notF. exact: contraTT H. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)