proposition: Lemma qperm'_Fix (s : seq A) (f g : forall y, (size y < size s)%N -> M (seq A)) : (forall y (p : (size y < size s)%N), f y p = g y p) -> qperm' f = qperm' g.
proof: Proof. move=> H; rewrite /qperm'; case: s f g H => // h t f g H. bind_ext => -[a b] /=. rewrite (_ : f = g) //; apply funext_dep => s. by apply boolp.funext => ?; exact: H. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)