(* 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. *)
(* 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. *)
notation "hvbox(n break ≃ m)"
non associative with precedence 45
for @{ 'congruent $n $m }.
notation "hvbox(n break ≃ m)"
non associative with precedence 45
for @{ 'congruent $n $m }.