update in standard library

[helm.git] / matita / matita / lib / tutorial / chapter12.ma

diff --git a/matita/matita/lib/tutorial/chapter12.ma b/matita/matita/lib/tutorial/chapter12.ma
index a4f47c1ffa7c38cca91315c5747385c9fb5a8628..07a5fd19f04586d76a2bfa627ede33b789a69c9d 100644 (file)
--- a/matita/matita/lib/tutorial/chapter12.ma
+++ b/matita/matita/lib/tutorial/chapter12.ma
@@ -16,6 +16,7 @@ include "basics/relations.ma".
 include "basics/types.ma".
 include "arithmetics/nat.ma".
 include "hints_declaration.ma".
+include "basics/core_notation/invert_1.ma".
 
 (******************* Quotienting in type theory **********************)
 
@@ -50,7 +51,7 @@ record setoid : Type[1] ≝ {
 (* Note that carrier has been defined as a coercion so that when S is a setoid
  we can write x:S in place of x: carrier S. *)
 
-(* We use the notation ≃ for the equality over setoid elements. *)
+(* We use the notation ≃ for the equality on setoid elements. *)
 notation "hvbox(n break ≃ m)"
   non associative with precedence 45
 for @{ 'congruent $n $m }.