diff --git a/library/init/logic.lean b/library/init/logic.lean
index 2a59fb859..b4bdf7e26 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -762,6 +762,9 @@ intro : (∀ a b : A, a = b) → subsingleton A
 protected definition subsingleton.elim {A : Type} [H : subsingleton A] : ∀(a b : A), a = b :=
 subsingleton.rec (λp, p) H
 
+protected definition subsingleton.helim {A B : Type} [H : subsingleton A] (h : A = B) (a : A) (b : B) : a == b :=
+by induction h; apply heq_of_eq; apply subsingleton.elim
+
 definition subsingleton_prop [instance] (p : Prop) : subsingleton p :=
 subsingleton.intro (λa b, !proof_irrel)
 
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 61c3c430c..980dadcd4 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -195,6 +195,7 @@ name const * g_string_str = nullptr;
 name const * g_sub = nullptr;
 name const * g_subsingleton = nullptr;
 name const * g_subsingleton_elim = nullptr;
+name const * g_subsingleton_helim = nullptr;
 name const * g_tactic = nullptr;
 name const * g_tactic_all_goals = nullptr;
 name const * g_tactic_and_then = nullptr;
@@ -458,6 +459,7 @@ void initialize_constants() {
     g_sub = new name{"sub"};
     g_subsingleton = new name{"subsingleton"};
     g_subsingleton_elim = new name{"subsingleton", "elim"};
+    g_subsingleton_helim = new name{"subsingleton", "helim"};
     g_tactic = new name{"tactic"};
     g_tactic_all_goals = new name{"tactic", "all_goals"};
     g_tactic_and_then = new name{"tactic", "and_then"};
@@ -722,6 +724,7 @@ void finalize_constants() {
     delete g_sub;
     delete g_subsingleton;
     delete g_subsingleton_elim;
+    delete g_subsingleton_helim;
     delete g_tactic;
     delete g_tactic_all_goals;
     delete g_tactic_and_then;
@@ -985,6 +988,7 @@ name const & get_string_str_name() { return *g_string_str; }
 name const & get_sub_name() { return *g_sub; }
 name const & get_subsingleton_name() { return *g_subsingleton; }
 name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
+name const & get_subsingleton_helim_name() { return *g_subsingleton_helim; }
 name const & get_tactic_name() { return *g_tactic; }
 name const & get_tactic_all_goals_name() { return *g_tactic_all_goals; }
 name const & get_tactic_and_then_name() { return *g_tactic_and_then; }
diff --git a/src/library/constants.h b/src/library/constants.h
index fb64c1f94..e5061ad1c 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -197,6 +197,7 @@ name const & get_string_str_name();
 name const & get_sub_name();
 name const & get_subsingleton_name();
 name const & get_subsingleton_elim_name();
+name const & get_subsingleton_helim_name();
 name const & get_tactic_name();
 name const & get_tactic_all_goals_name();
 name const & get_tactic_and_then_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 93cfbd659..2788cf005 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -190,6 +190,7 @@ string.str
 sub
 subsingleton
 subsingleton.elim
+subsingleton.helim
 tactic
 tactic.all_goals
 tactic.and_then