proposition: Lemma eqb_true_False : forall (A : Set)(eqd : EqDec A) (a1 a2 : A), (eqb a1 a2 = true -> False) -> a1 <> a2.
proof: Proof. intuition. subst. eapply H. eapply eqb_refl. Qed.
imports: FCF.Rat FCF.Comp FCF.DistRules FCF.DistSem FCF.StdNat FCF.Fold FCF.NotationV1