proposition: Lemma pARE2 w v : pAR e p q w -> ~~ p w -> e w v -> pAR e p q v.
proof: Proof. move => Hw pw wv pi p1 p2 n. case/(_ _ (erefl _))/Wrap: (@Hw (pcons w pi)). apply: path_pcons => //; congruence. move/(_ n.+1) => /=. intuition. case: H => [[|m]] Hm Hm'. - by rewrite /= (negbTE pw) in Hm'. - left. by exists m. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)