proposition: Lemma supp_eval s x : val x |> s -> eval (interp s) x.
proof: Proof. case: s x. elim => [|p|s IHs t IHt|s IHs|s IHs] [|] x. - by rewrite /= (LCF (ssvalP x)). - by rewrite /=. - done. - rewrite /= /Mlabel. case: (LCF (ssvalP x)) => [_ /(_ p)]. by case: (_^+ \in _) => //= ->. - rewrite /=. case/orP => [/IHs|/IHt] /=; tauto. - rewrite /=. case/andP => [/IHs ? /IHt] /=; tauto. - move => inX y xy. apply: (IHs true). rewrite -suppC1. apply: suppC_sub xy. by rewrite fsub1 RE. - rewrite [_ |> _]/= => H. case/hasP : (demoD1 (ssvalP x) H) => D inS. rewrite suppCU suppC1 => /andP [D1 D2] /= /(_ (Sub D inS)) /(_ D2). exact: (IHs false). - move: x. cofix supp_eval => x. rewrite [_ |> _]/= => /andP [X1 X2]. apply: AGs => [|y xy]; [exact: IHs X1|apply: supp_eval]. rewrite -suppC1. apply: suppC_sub xy. by rewrite fsub1 RE. - move => H. apply: cAG_cEF. apply: EF_strengthen (IHs false) _. move: H. rewrite [_ |> _]/=. case/orP => [?|]; first exact: EF0. move/(demoD2 (ssvalP x)). case: x => C inS supp. rewrite /= in supp. elim: supp inS => {C} - C D DinS CD. + move => Ds inS. apply: (EFs (v := Sub D DinS)) => //. exact: EF0. + move => _ IH inS. apply: (EFs (v := Sub D DinS)) => //. exact: IH. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)