diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts
index fe79e35..c321de7 100644
--- a/frontend/src/mathjax-proof-tree.ts
+++ b/frontend/src/mathjax-proof-tree.ts
@@ -443,6 +443,7 @@ class MathjaxProofTree extends MathjaxAdapter {
                             .then(() => {
                                 const svgP = p.getElementsByTagName("svg")[0];
                                 const relevantElement = svgP.childNodes[1]! as SVGGraphicsElement;
+                                const relevantElementBox = relevantElement.getBBox();
                                 const relevantDefs = svgP.childNodes[0]!;
                                 const ourDefs = svg.getElementsByTagName("defs")[0];
                                 while (relevantDefs.childNodes.length > 0) {
@@ -454,24 +455,19 @@ class MathjaxProofTree extends MathjaxAdapter {
                                 for (const explainer of explainers) {
                                     explainer.parentNode!.removeChild(explainer);
                                 }
-                                relevantElement.classList.add(hoverTextElID);
-                                const x = String(-transform.e - svgRect.width + 30500);
-                                const y = -transform.f - 4000;
-                                const prevTransform = relevantElement.getAttribute("transform");
-                                const newTranslate = "translate(" + x + ", " + y + ")";
-                                const newTransform = prevTransform + " " + newTranslate;
-                                relevantElement.setAttribute("transform", newTransform);
+                                const g = insertionTarget.ownerDocument.createElementNS("http://www.w3.org/2000/svg", "g");
+                                g.setAttribute("transform", "matrix(1 0 0 -1 0 0)");
+                                g.transform.baseVal[0].matrix.f -= relevantElementBox.height / 2 + svgRect.height;
                                 let ttBackground = document.createElementNS("http://www.w3.org/2000/svg", "rect");
-                                ttBackground.classList.add(hoverTextElID);
+                                g.classList.add(hoverTextElID);
                                 const bbox = relevantElement.getBBox();
-                                const newTranslate2 = "translate(" + x + ", " + (y - bbox.height / 2) + ")";
-                                const newTransform2 = prevTransform + " " + newTranslate2;
-                                ttBackground.setAttribute("transform", newTransform2);
                                 ttBackground.setAttribute("width", String(bbox.width + 2000));
                                 ttBackground.setAttribute("height", String(bbox.height + 1000));
+                                ttBackground.setAttribute("transform", "translate(0 " + String(-bbox.height + 600) + ")");
                                 ttBackground.setAttribute("fill", "yellow");
-                                insertionTarget.appendChild(ttBackground);
-                                insertionTarget.appendChild(relevantElement);
+                                g.appendChild(ttBackground);
+                                g.appendChild(relevantElement);
+                                defEl.appendChild(g);
                                 thisShadowRoot.removeChild(p);
                             });
                         this.shadowRoot!.appendChild(p);
diff --git a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
index 4bc0e84..6ee6c7f 100644
--- a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
+++ b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
@@ -75,14 +75,13 @@ public class StepAnnotator implements StepVisitor {
 
     @Override
     public void visit(ConstStepDefault constD) {
-        visitGeneric2(List.of(Pair.of("_c", constD.getConclusion().getType())), constD.getConstraint());
+        visitGeneric2(List.of(Pair.of("", constD.getConstraint().getSecondType())), constD.getConstraint());
     }
 
     @Override
     public void visit(VarStepDefault varD) {
         visitGeneric2(List.of(
-                Pair.of("", varD.getInstantiatedTypeAbs()),
-                Pair.of("'", varD.getConclusion().getType())),
+                Pair.of("", varD.getInstantiatedTypeAbs())),
                 varD.getConstraint());
     }
 
diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties
index 02ea1f3..21446da 100644
--- a/src/main/resources/language/general.properties
+++ b/src/main/resources/language/general.properties
@@ -16,7 +16,7 @@ root.exampleTerms=\
   (λx.λy.y (x y)) (λz. λa. z g a),\
   let f = λx. let g = λy. y in g x in f 3,\
   let f = λx. let g = λy.5 5 in g x in f 3
-  
+
 root.λx.x=∅
 root.λx.λy.yx=∅
 root.(λx.xtrue)(yg)=∅;y: int->boolean->τ₁, g: boolean;y: int->boolean->τ₁, g: τ₁;y: int->boolean->τ₁, g: ∀τ₁.τ₁
@@ -27,7 +27,7 @@ root.(λx.xx)(λx.xx)=∅
 root.(λx.λy.y(xy))(λz.λa.zga)=∅;g: boolean;a: int, g: boolean->int;g: ∀τ₂.τ₁->τ₂
 root.letfλx.letgλy.yingxinf3=∅;g: boolean->int->boolean
 root.letfλx.letgλy.55ingxinf3=∅
- 
+
 root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2329Abs\u232A | \
 \u2329Let\u232A | \u2329Var\u232A | \u2329Const\u232A <br> \
 \u2329App\u232A ::= \u2329Term\u232A \u2329Term\u232A <br> \
@@ -68,7 +68,7 @@ root.varLatex=\
 \\AxiomC{$\\Gamma (\\texttt{x}) = \\tau$}\
 \
 \\LeftLabel{\\textrm V{\\small AR}}\
-\\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau'$}\
+\\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\
 \\end{prooftree}
 
 root.constLatex=\
@@ -76,7 +76,7 @@ root.constLatex=\
 \\AxiomC{$\\texttt{c} \\in Const$}\
 \
 \\LeftLabel{\\textrm C{\\small ONST}}\
-\\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau_c$}\
+\\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau$}\
 \\end{prooftree}
 
 root.letLatex=\