compilation fix

src/Tutorial/C_Proofs.lagda.md

@@ -152,8 +152,8 @@ MyLang-is-Complete' m =
 We do not recommend doing this by hand because it is very tedious.
 In the framework, we did it by first proving
 ```agda
-_ : Complete VariantList.VariantListL
-_ = VariantList-is-Complete "🍇"
+_ : Complete (VariantList.VariantListL V)
+_ = VariantList-is-Complete "🍇" V
 ```
 and then translating `VariantList`s to the other languages,
 and proving completeness via `completeness-by-expressiveness` again.
@@ -202,8 +202,8 @@ and then translate our language to it.
 Soundness can also be proven directly, but this is again cumbersome, and we
 only proved it directly for `VariantList` just as we did for completeness.
 ```agda
-_ : Sound VariantList.VariantListL
-_ = VariantList-is-Sound
+_ : Sound (VariantList.VariantListL V)
+_ = VariantList-is-Sound V
 ```
 
 </details>