Different types of equality in F*

Equalities

F* has 3 different types of equality:

val (=)  : #a:Type{hasEq a} -> a -> a -> Tot bool
val (==) : #a:Type -> a -> a -> Tot Type0
val (===): #a:Type -> #b:Type -> a -> b -> Tot Type0

Here is what each of them means:

= is boolean equality that is automatically generated by F* for many types with decidable equality; such types satisfy the hasEq predicate.
== is homogeneous propositional equality, and is defined for all F* types, even the ones without hasEq (== is defined in prims.fst as a squashed inductive)
=== is heterogeneous propositional equality; this more exotic equality is sometimes called "John Major equality" (=== is defined in prims.fst as a squashed inductive)

Corresponding to the equalities, there are also the corresponding disequalities :

x <> y is equivalent to not (x = y) (the decidable boolean valued disequality)
x =!= y is equivalent yo ~(x == y) (the logical, homogeneous disequality)