Goal:
    G : t  HI : invariants
  ============================
   (VSet.For_all (fun x : VSet.elt => lsp x x = Some 0) (V G) <->
    VSet.For_all
      (fun x : VSet.elt =>
       (fun x0 : VSet.elt =>
        match lsp x0 x0 with
        | Some 0 => true
        | _ => false
        end) x = true) (V G))


DEBUG:Going to execute:
apply iff_forall