Goal:
    G : t  HI : invariants
  ============================
   (Proper (eq ==> eq)
      (fun x : VSet.elt =>
       match lsp x x with
       | Some 0 => true
       | _ => false
       end))


DEBUG:Going to execute:
intros x y []
DEBUG LTAC Evaluated term: VSetFact.for_all_iff