proposition: Lemma v_sup n m I J (f: I -> expr3 n m): v (sup f J) = \sup_(i\in J) (v (f i)).
proof: Proof. apply f_sup_eq; now f_equal. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms