proposition: Lemma afn1 (s : form) : mprv ([af [fset s^-]] ---> Neg s).
proof: Proof. change (Neg s) with (interp (s^-)). apply: bigAE. by rewrite !inE. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert)