proposition: Corollary classical_soundness (dn: forall P , ~ ~ P -> P) s: prv s -> forall (M: ts) (v: M), eval s v.
proof: Proof. move => H M v. have stable_ts: stable (@eval M). move => t w. exact: dn. exact: (@soundness _ H (CModel stable_ts)). Qed.
imports: Relations Lia Setoid Morphisms mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype rewrite_inequality fset_tac)