proposition: Lemma lowDistApprox_left_total : forall (A : Set)(eqd : eq_dec A)(c : Comp A) a, well_formed_comp c -> left_total (lowDistApprox c a).
proof: Proof. unfold left_total. intuition. destruct (@dat_exists n _ c). trivial. exists (lowDistApproxFromTree eqd x a). eapply low_tree_approx_same. trivial. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat