proposition: Lemma dirac_refl n: dirac n n = 1.
proof: Proof. unfold dirac. case eqb_pos_spec. 2: congruence. intro. now rewrite cmp_eq_rect_eq. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms