proposition: Lemma qperm_isNondet A (s : seq A) : plus_isNondet (qperm s : M _).
proof: Proof. have [n sn] := ubnP (size s); elim: n s => // n ih s in sn *. move: s => [|h t] in sn *; first by exists (ndRet [::]); rewrite qperm_nil. rewrite qperm_cons splits_bseqE fmapE bindA. have [syn syn_tsplits] := splits_bseq_isNondet t. have liftM2_qperm_isNondet (a b : (size t).-bseq A) : plus_isNondet (liftM2 (fun x y => x ++ h :: y) (qperm a) (qperm b : M _)). apply: liftM2_isNondet => //; apply: ih. - by rewrite (leq_ltn_trans (size_bseq a)). - by rewrite (leq_ltn_trans (size_bseq b)). exists (ndBind syn (fun a => sval (liftM2_qperm_isNondet a.1 a.2))). rewrite /= syn_tsplits; bind_ext => -[a b] /=. by rewrite bindretf; case: (liftM2_qperm_isNondet _ _). Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)