diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index 3777f6d2c..3608f41df 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -232,6 +232,9 @@ namespace eq
     : p₁₂ = p₀₁⁻¹ ⬝ p₁₀ ⬝ p₂₁ :=
   by induction s₁₁; apply idp
 
+  definition square_of_eq_bot (r : p₀₁⁻¹ ⬝ p₁₀ ⬝ p₂₁ = p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ :=
+  by induction p₂₁; induction p₁₀; esimp at r; induction r; induction p₀₁; exact ids
+
   definition square_equiv_eq [constructor] (t : a₀₀ = a₀₂) (b : a₂₀ = a₂₂)
     (l : a₀₀ = a₂₀) (r : a₀₂ = a₂₂) : square t b l r ≃ t ⬝ r = l ⬝ b :=
   begin
diff --git a/hott/homotopy/smash.hlean b/hott/homotopy/smash.hlean
index 0130fdc20..194451970 100644
--- a/hott/homotopy/smash.hlean
+++ b/hott/homotopy/smash.hlean
@@ -8,7 +8,7 @@ The Smash Product of Types
 
 import hit.pushout .wedge .cofiber .susp .sphere
 
-open eq pushout prod pointed Pointed
+open eq pushout prod pointed Pointed is_trunc
 
 definition product_of_wedge [constructor] (A B : Type*) : Wedge A B →* A ×* B :=
 begin
@@ -23,7 +23,30 @@ open sphere susp unit
 
 namespace smash
 
-  definition smash_bool (X : Type*) : Smash X Bool ≃* X :=
+  protected definition prec {X Y : Type*} {P : Smash X Y → Type}
+    (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆))
+    (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y)))
+    (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y))
+    (pg : pathover (λ x, pathover P ps (glue x) (@prod.rec X Y (λ x, P (inr x)) pxy
+          (pushout.elim (λ a, (a, Point Y)) (pair (Point X)) (λ x, idp) x)))
+          (px (Point X)) (glue ⋆) (py (Point Y))) : Π s, P s :=
+  begin
+    intro s, induction s, induction x, exact ps,
+    induction x with [x, y], exact pxy x y,
+    induction x with [x, y, u], exact px x, exact py y,
+    induction u, exact pg,
+  end
+
+  protected definition prec_on {X Y : Type*} {P : Smash X Y → Type} (s : Smash X Y)
+    (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆))
+    (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y)))
+    (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y))
+    (pg : pathover (λ x, pathover P ps (glue x) (@prod.rec X Y (λ x, P (inr x)) pxy
+          (pushout.elim (λ a, (a, Point Y)) (pair (Point X)) (λ x, idp) x)))
+          (px (Point X)) (glue ⋆) (py (Point Y))) : P s :=
+  smash.prec pxy ps px py pg s
+
+/-  definition smash_bool (X : Type*) : Smash X Bool ≃* X :=
   begin
     fconstructor,
     { fconstructor,
@@ -38,24 +61,23 @@ namespace smash
     { fapply is_equiv.adjointify,
       { intro x, apply inr, exact pair x bool.tt },
       { intro x, reflexivity },
-      { intro s, esimp, induction s, } }
-  end
-
-  check ap_compose
-
-
-  check bool.rec
-
-exit
-fconstructor, intro x, induction x, exact point X,
-      induction a, exact point X, esimp, induction x, do 2 reflexivity, 
-      apply eq_pathover, apply hdeg_square, induction x, -/
-
+      { intro s, esimp, induction s,
+        { cases x, apply (glue (inr bool.tt))⁻¹ },
+        { cases x with [x, b], cases b, 
+          apply inverse, apply concat, apply (glue (inl x))⁻¹, apply (glue (inr bool.tt)),
+          reflexivity }, 
+        { esimp, apply eq_pathover, induction x, 
+          esimp, apply hinverse, krewrite ap_id, apply move_bot_of_left, 
+          krewrite con.right_inv,
+          refine _ ⬝hp !(ap_compose (λ a, inr (pair a _)))⁻¹,
+          apply transpose, apply square_of_eq_bot, rewrite [con_idp, con.left_inv],
+          apply inverse, apply concat, apply ap (ap _), 
+           } } }
 
   definition susp_equiv_circle_smash (X : Type*) : Susp X ≃* Smash (Sphere 1) X :=
   begin
     fconstructor,
     { fconstructor, intro x, induction x, },
-  end
+  end-/
 
 end smash