proposition: Theorem evalDist_1 : forall (A : Set)(eqd : EqDec A)(c : Comp A) a, well_formed_comp c -> evalDist c a == 1 -> (getSupport c) = (a :: nil)%list.
proof: Proof. intuition. specialize (evalDist_getSupport_perm_id c (ret a)); intuition. assert (forall a0 : A, evalDist c a0 == evalDist (ret a) a0). intuition. case_eq (eqb a a0); intuition. rewrite eqb_leibniz in H2. subst. simpl. destruct (EqDec_dec eqd a0 a0); intuition. simpl. assert (evalDist c a0 == 0). eapply evalDist_1_0; intuition. eapply H0. subst. rewrite eqb_refl in H2. discriminate. rewrite H3. destruct ( EqDec_dec eqd a a0); subst; intuition. rewrite eqb_refl in H2. discriminate. intuition. simpl in *. eapply Permutation_length_1_inv. eapply Permutation_sym. trivial. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia