theorem
WGCL.wGCL.wp_le_of_le
{D M W Var : Type}
[DecidableEq Var]
[Monoid W]
[AddCommMonoid M]
[DistribMulAction W M]
[(B : BExpr D Var) → (σ : Mem D Var) → Decidable (B σ)]
[OmegaCompletePartialOrder M]
[OrderBot M]
[AddLeftMono M]
[CovariantClass W M HSMul.hSMul LE.le]
{φ : BExpr D Var}
{f : Weighting D M Var}
{C : wGCL D W Var}
(I : Weighting D M Var)
(h : (Φ φ C f) I ≤ I)
:
Park induction