proposition: Lemma datCorrect_datDepth : forall (A : Set)(c : Comp A) n t, dat_correct c n t -> (datDepth t <= n)%nat.
proof: Proof. induction 1; intuition; simpl in *. destruct (le_dec (datDepth t1) (datDepth t2)). rewrite Nat.max_r; eauto. lia. rewrite Nat.max_l; lia. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat