proposition: Lemma datRepeat_depth_0 : forall n2 n1 (A : Set)(f : nat -> DistApproxTree A -> Prop) P t1 t2, datRepeat_depth f P n1 O t1 t2 -> n2 >= n1 -> f O (dat_leaf None) -> datRepeat_depth f P n2 O t1 t2.
proof: Proof. induction n2; intuition; subst. inversion H; clear H; subst. econstructor. econstructor. trivial. econstructor. trivial. trivial. lia. inversion H; clear H; subst. econstructor. econstructor; trivial. econstructor. trivial. eauto. econstructor. econstructor; eauto. eapply IHn2; eauto. lia. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat