diff --git a/BasicSyntax.v b/BasicSyntax.v index 37bc3b0..1c56c5c 100644 --- a/BasicSyntax.v +++ b/BasicSyntax.v @@ -168,7 +168,7 @@ Module ArithWithVariables. end. Compute depth ex1. - Compute size ex2. + Compute depth ex2. Theorem depth_le_size : forall e, depth e <= size e. Proof.