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