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] [|] x. - by rewrite /= (LCF (demoD0 (ssvalP x))). - by rewrite /=. - done. - rewrite /= /Mlabel. case: (LCF (demoD0 (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). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def)