proposition: Lemma datRepeat_func_eq : forall n (A : Set)(t1 t2 : DistApproxTree A) f P (P' : DistApproxTree A -> Prop), datRepeat f P n t1 t2 -> (forall t, f t -> P' t) -> datRepeat P' P n t1 t2.
proof: Proof. induction 1; intuition; simpl in *. econstructor. econstructor. trivial. econstructor. trivial. econstructor. eapply H2. eauto. trivial. trivial. econstructor; trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat