(vect2_metric_space
 (IMP_metric_spaces_TCC1 0
  (IMP_metric_spaces_TCC1-2 nil 3476029485
   ("" (expand "metric_space?")
    (("" (prop)
      (("1" (expand "space_zero?")
        (("1" (skosimp*)
          (("1" (lemma "dist_eq_0")
            (("1" (inst - "x!1" "y!1") nil nil)) nil))
          nil))
        nil)
       ("2" (expand "space_symmetric?")
        (("2" (skosimp*)
          (("2" (lemma "dist_sym") (("2" (inst - "x!1" "y!1") nil nil))
            nil))
          nil))
        nil)
       ("3" (expand "space_triangle?")
        (("3" (skosimp*)
          (("3" (lemma "dist_triangle")
            (("3" (inst - "x!1" "y!1" "z!1") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (dist_eq_0 formula-decl nil distance_2D "vectors/")
    (space_zero? const-decl "bool" metric_spaces_def "analysis/")
    (dist_sym formula-decl nil distance_2D "vectors/")
    (space_symmetric? const-decl "bool" metric_spaces_def "analysis/")
    (dist_triangle formula-decl nil distance_2D "vectors/")
    (space_triangle? const-decl "bool" metric_spaces_def "analysis/")
    (metric_space? const-decl "bool" metric_spaces_def "analysis/"))
   nil)
  (IMP_metric_spaces_TCC1-1 nil 3476029427 ("" (assuming-tcc) nil nil)
   nil nil))
 (vect2_subset_metric_space 0
  (vect2_subset_metric_space-1 nil 3476029531
   ("" (skosimp*)
    (("" (expand "metric_space?")
      (("" (prop)
        (("1" (expand "space_zero?")
          (("1" (skosimp*)
            (("1" (lemma "dist_eq_0")
              (("1" (inst - "x!1" "y!1") nil nil)) nil))
            nil))
          nil)
         ("2" (expand "space_symmetric?")
          (("2" (skosimp*)
            (("2" (lemma "dist_sym")
              (("2" (inst - "x!1" "y!1") nil nil)) nil))
            nil))
          nil)
         ("3" (expand "space_triangle?")
          (("3" (skosimp*)
            (("3" (lemma "dist_triangle")
              (("3" (inst - "x!1" "y!1" "z!1") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((metric_space? const-decl "bool" metric_spaces_def "analysis/")
    (space_triangle? const-decl "bool" metric_spaces_def "analysis/")
    (dist_triangle formula-decl nil distance_2D "vectors/")
    (space_symmetric? const-decl "bool" metric_spaces_def "analysis/")
    (dist_sym formula-decl nil distance_2D "vectors/")
    (space_zero? const-decl "bool" metric_spaces_def "analysis/")
    (dist_eq_0 formula-decl nil distance_2D "vectors/")
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil))
   nil))
 (vect2_metric_space 0
  (vect2_metric_space-1 nil 3476029555
   ("" (lemma "vect2_subset_metric_space")
    (("" (inst - "fullset[Vect2]") nil nil)) nil)
   ((real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (vect2_subset_metric_space formula-decl nil vect2_metric_space
     nil))
   nil)))