diff --git a/.gitignore b/.gitignore
index 0ff75ef4..ba35be6a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,7 @@ docs/build/
 *.hi
 *.o
 
+# For nix users
+.direnv/**
+.envrc
+result
diff --git a/tutorials/example-proofs/Ascending.agda b/tutorials/example-proofs/Ascending.agda
index 288f52c2..dd492294 100644
--- a/tutorials/example-proofs/Ascending.agda
+++ b/tutorials/example-proofs/Ascending.agda
@@ -1,7 +1,9 @@
 module Ascending where
 
 open import Haskell.Prelude
-open import Haskell.Prim 
+open import Haskell.Prim
+open import Haskell.Law.Equality using (sym; begin_; _≡⟨⟩_; step-≡; _∎)
+open import Haskell.Law.Bool using (ifTrueEqThen)
 
 -- function judging ascending order on lists
 isAscending : ⦃ iOrdA : Ord a ⦄ → List a → Bool
diff --git a/tutorials/example-proofs/Triangle.agda b/tutorials/example-proofs/Triangle.agda
index 57b3e05d..6938bccb 100644
--- a/tutorials/example-proofs/Triangle.agda
+++ b/tutorials/example-proofs/Triangle.agda
@@ -1,6 +1,7 @@
 module Triangle where
 
 open import Haskell.Prelude
+open import Haskell.Law.Bool using (&&-rightTrue; &&-leftTrue)
 
 -- helper function
 countBiggerThan : ⦃ Ord a ⦄ → List a → a → Int