proposition: Lemma refine_Count_bind_bind_app {A} : forall (l l' : Comp (list A)), refine (Count (la <- l; la' <- l'; {l | Permutation.Permutation (la ++ la') l})) (len <- Count l; len' <- Count l'; ret (len + len')).
proof: Proof. intros; unfold Count. unfold refine; intros; computes_to_inv; subst. computes_to_econstructor; eauto. rewrite app_length; computes_to_econstructor. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure