proposition: Lemma elim_hoare_hypotheses_leq `{L: laws} {n m p q} (u: X n p) (v: X q m) (z: X p q) (x y: X n m): z ≦ 0 -> x ≦ y+u⋅z⋅v -> x ≦y.
proof: Proof. intro Hz. now rewrite Hz, dotx0, dot0x, cupxb. Qed.
imports: boolean ugregex_dec kat_reification kat_untyping kat_completeness