proposition: Lemma evaldP (M : dmodel) (x:M) s : reflect (@eval (ts_of_dmodel M) s x) (evald s x).
proof: Proof. elim: s x => //=. - by constructor. - move => * ; exact: idP. - move => s IHs t IHt w. apply: iffP (@implyP _ _) _ _ => ? /IHs ?; apply/IHt; firstorder. - move => s IHs w. apply: iffP (@all_inP _ _ _ _) _ _ => [H v wv|H v _ wv]. + apply/IHs. apply: H => //. exact: dtransP. + apply/IHs. exact: H. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)