proposition: Lemma traces_deriv_single a i j: traces_deriv a i (tsingle j) ≡ ofbool (eqb i j).
proof: Proof. intros [b|???]. unfold traces_deriv. simpl. case eqb_spec; simpl; intuition; discriminate. unfold traces_deriv. simpl. case eqb_spec; reflexivity. Qed.
imports: prop monoid positives comparisons