proposition: Lemma symbols_size_is_fold : symbols \o (@size_Tree Symbol) = foldt drTip drBin.
proof: Proof. apply foldt_universal. by rewrite -compA (_ : @size_Tree Symbol \o _ = const 1) // symbols_prop1. pose p := @distinct _ M. transitivity (bassert p \o symbols \o @size_Tree Symbol \o uncurry Bin : (_ -> M _)). by rewrite bassert_symbols. transitivity ((bassert p) \o symbols \o uaddn \o (@size_Tree Symbol)^`2 : (_ -> M _)). by rewrite -[in LHS]compA -[in RHS]compA size_Tree_Bin. transitivity (bassert p \o (fmap ucat) \o mpair \o (symbols \o (@size_Tree Symbol))^`2 : (_ -> M _)). rewrite -2!compA (compA symbols) symbols_prop2. by rewrite -(compA (_ \o mpair)) (compA (bassert p)). transitivity ((fmap ucat) \o bassert q \o mpair \o (bassert p \o symbols \o (@size_Tree Symbol))^`2 : (_ -> M _)). by rewrite (promote_assert_sufficient_condition (@failfresh_bindmfail _ M) promotable_q). transitivity ((fmap ucat) \o bassert q \o mpair \o (symbols \o (@size_Tree Symbol))^`2 : (_ -> M _)). by rewrite bassert_symbols. by []. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib