proposition: Lemma plp l: pl (lp l) = l.
proof: Proof. destruct l; unfold pl, lp; now rewrite !get_mk_sum, ?get_mk_pair, ?get_mk_ord. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms