theorem
WGCL.wGCL.op_eq_wp
{D M W Var : Type}
[DecidableEq Var]
[DecidableEq (wGCL D W Var)]
[TopologicalSpace M]
[Monoid W]
[AddCommMonoid M]
[DistribMulAction W M]
[Zero W]
[(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)]
[OmegaCompletePartialOrder M]
[OrderBot M]
[AddLeftMono M]
[CovariantClass W M HSMul.hSMul LE.le]
{C : wGCL D W Var}
: