proposition: Lemma demo2reach p c d : (forall t e, sizef t < sizep p -> t^+ \in val e -> eval t e) -> reach_demo S p (val c) (val d) -> reach p c d.
proof: Proof. elim : p c d => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp|s|p IHp] c d //= Ht. - move/orP => [H|H];[left; apply: IH0|right;apply: IH1] => // t e ?; apply Ht; by ssrlia. - move/hasP => [C' inS /andP [L R]]. exists (SeqSub C' inS). + apply IH0 => // t e ?. by apply: Ht; ssrlia. + apply IH1 => // t e ?. by apply: Ht; ssrlia. - case/connect_inP => cs. elim: cs c d => /= [|e cd IH] c d. + case => _ _ /eqP. rewrite -[_ d == _ c]/(d == c) => /eqP->. by constructor. + case => /and3P[A B C] /andP[D E] F. apply: (StarL (z := SeqSub e B)). * apply: IHp => // t e' E'. apply: Ht; ssrlia. * apply IH. by rewrite /= B C E F. - rewrite -[_ c == _ d]/(c == d) => /andP[/eqP-> A]. split => //. by apply: Ht A; ssrlia. - apply: IHp => t e ?. by apply: Ht; ssrlia. Qed.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.CPDL(PDL_def)