vstd::laws_eq

Function obeys_deep_eq

Source 
pub open spec fn obeys_deep_eq<T: PartialEq + DeepView>() -> bool
Expand description
{
    &&& T::obeys_eq_spec()
    &&& forall |x: T, y: T| x.eq_spec(&y) <==> x.deep_view() == y.deep_view()

}