diff --git a/Javascript/f.html b/Javascript/f.html
index bd855c47d7b2872a0f702865417453ad1164c165..618b30ccfad6083d3643d9bfcaf46d35265db399 100755
--- a/Javascript/f.html
+++ b/Javascript/f.html
@@ -28,6 +28,15 @@
 						this.term2 = arg2;
 					}
 				}
+				print()
+				{
+					if(this.kind === "var")
+						return this.value.toString();
+					if(this.kind === "abs")
+						return "∀." + this.term.print();
+					if(this.kind === "app")
+						return "(" + this.term1.print() + ")" + this.term2.print();
+				}
 				lift(index = 0)
 				{
 					if(this.kind === "var")
@@ -92,6 +101,23 @@
 						this.stack = arg2;
 					}
 				}
+				print()
+				{
+					if(this.kind === "var")
+						return this.value.toString();
+					if(this.kind === "abs")
+					{
+						return "λ:" + this.type.print() + "." + this.term.print();
+					}
+					if(this.kind === "app")
+						return "(" + this.term1.print() + ")" + this.term2.print();
+					if(this.kind === "tabs")
+					{
+						return "Λ" + this.term.print();
+					}
+					if(this.kind === "tapp")
+						return "(" + this.term1.print() + ")" + this.term2.print();
+				}
 				get_type(context = [])
 				{
 					if(this.kind === "var")
@@ -248,6 +274,25 @@
 						this.forms = arg1;
 					if(kind === "other") {}
 				}
+				print()
+				{
+					if(this.kind === "atom")
+					{
+						return this.term.print() + "∈" + this.set;
+					}
+					if(this.kind === "forall")
+						return "∀(" + this.form.print() + ")";
+					if(this.kind === "forall2")
+						return "∀2(" + this.form.print() + ")";
+					if(this.kind === "impl")
+					{
+						return "(" + this.form1.print() + ")⇒(" + this.form2.print() + ")";
+					}
+					if(this.kind === "conj")
+						return this.forms.map(f => f.print()).join("∧");
+					if(this.kind === "other")
+						return "@";
+				}
 				subst(term, index = 0)
 				{
 					if(this.kind === "atom")
@@ -317,7 +362,7 @@
 						return new Formula("other");
 				}
 			}
-			let norm =  new Formula("impl", new Formula("forall", new Formula("impl", new Formula("other"), new Formula("other"))), new Formula("other"));
+			let norm =  new Formula("impl", new Formula("forall", new Formula("other")), new Formula("other"));
 			let redcand =  new Formula("conj", [
 				new Formula("forall", new Formula("atom", new Term("meta_app", new Term("var", 0), new Term("meta_var", 0)), 0)),
 				new Formula("forall", new Formula("impl", new Formula("atom", new Term("meta_var", 0), 0), norm)),
@@ -359,7 +404,20 @@
 				if(form.kind === "other")
 					return [y => y, y => y];
 			}
-			let brec = f => g => s => g(x => s(x) === null ? f(y => brec(f)(g)(z => Term.equal(z, x) ? y : s(z))) : s(x));
+			let brec = f => g => form =>
+			{
+				let n = document.getElementById("parse_alert").appendChild(document.createElement("div")).appendChild(document.createTextNode(""));
+				let brec_aux = s =>
+				{
+					n.textContent = form.print() + ":";
+					for (let [key, value] of s)
+					{
+						n.textContent += key + ";";
+					}
+					return g(x => s.has(x.print()) ? s.get(x.print()) : f(y => brec_aux(new Map(s).set(x.print(), y))));
+				}
+				return brec_aux;
+			}
 			let dne = function(form)
 			{
 				if(form.kind === "atom")
@@ -381,7 +439,7 @@
 			}
 			let comp = function(form)
 			{
-				return y => brec(x => exf(new Formula("conj", [new Formula("impl", new Formula("atom", new Term("var", 0), 0), form), new Formula("impl", form, new Formula("atom", new Term("var", 0), 0))]))(x([exf(form), u => x([z => u, z => 0])])))(y)(x => null)
+				return y => brec(x => exf(new Formula("conj", [new Formula("impl", new Formula("atom", new Term("var", 0), 0), form), new Formula("impl", form, new Formula("atom", new Term("var", 0), 0))]))(x([exf(form), u => x([z => u, z => 0])])))(y)(form)(new Map())
 			}
 			let elim = function(form1, form2)
 			{
@@ -530,7 +588,7 @@
 		<div>
 			<input type=text id=type_txt size=100 onkeypress=if(event.which===13){parse()} />
 			<input type=button value=Parse onclick=parse() />
-			<span id=parse_alert style=color:red ></span>
+			<div id=parse_alert style=color:red ></div>
 		</div>
 		<div style=font-style:italic>(you can use "\" instead of "λ" and "^" instead of "∀")</div>
 		<br/>