proposition: Lemma elim_hoare_hypotheses_weq `{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+u⋅z⋅v ≡ y+u⋅z⋅v -> x ≡y.
proof: Proof. rewrite leq_xb_iff. intro Hz. now rewrite Hz, dotx0, dot0x, 2cupxb. Qed.
imports: boolean ugregex_dec kat_reification kat_untyping kat_completeness