proposition: Lemma supp_eval s (x : UM) : val x |> s -> eval (interp s) x.
proof: Proof. case: s x. elim => [|p|s IHs t IHt|s IHs] [|] x. - by rewrite /= (LCF (gen_lcons (valP x))). - by rewrite /=. - done. - rewrite /= /UMLabel. case: (LCF (gen_lcons (valP 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 (UM_trans_R xy). by rewrite fsub1 RE. - rewrite [_ |> _]/= => H. case: (UM_trans_D H) => y xy Hy. move/(_ y xy). exact: (IHs false). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)